harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Set/Image.lean
theorem preimage_inr_image_inl (s : Set α) : Sum.inr ⁻¹' (@Sum.inl α β '' s) = ∅

Proof state:
α : Type u_1
β : Type u_2
s : Set α
⊢ Sum.inr ⁻¹' (Sum.inl '' s) = ∅

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
s : Set α
x✝ : β
⊢ x✝ ∈ Sum.inr ⁻¹' (Sum.inl '' s) ↔ x✝ ∈ ∅

Proof state:
case h
α : Type u_1
β : Type u_2
s : Set α
x✝ : β
⊢ x✝ ∈ Sum.inr ⁻¹' (Sum.inl '' s) ↔ x✝ ∈ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Parity.lean
@[simp] lemma not_odd_iff_even : ¬Odd n ↔ Even n

Proof state:
n : ℤ
⊢ ¬Odd n ↔ Even n

Tactic:
rw [not_odd_iff, even_iff]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialNerve.lean
lemma functor_comp {J K L : Type u} [LinearOrder J] [LinearOrder K]
    [LinearOrder L] (f : J →o K) (g : K →o L) :
    functor (g.comp f) =
      (functor f).comp _ (functor g)

Proof state:
J K L : Type u
inst✝² : LinearOrder J
inst✝¹ : LinearOrder K
inst✝ : LinearOrder L
f : J →o K
g : K →o L
⊢ functor (g.comp f) = EnrichedFunctor.comp SSet (functor f) (functor g)

Tactic:
refine EnrichedFunctor.ext _ (fun _ ↦ rfl) fun i j ↦ ?_

Result:
J K L : Type u
inst✝² : LinearOrder J
inst✝¹ : LinearOrder K
inst✝ : LinearOrder L
f : J →o K
g : K →o L
i j : SimplicialThickening J
⊢ (functor (g.comp f)).map i j ≫ eqToHom ⋯ = (EnrichedFunctor.comp SSet (functor f) (functor g)).map i j

Proof state:
J K L : Type u
inst✝² : LinearOrder J
inst✝¹ : LinearOrder K
inst✝ : LinearOrder L
f : J →o K
g : K →o L
i j : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
a✝ : (EnrichedCategory.Hom i j).obj n✝
⊢ ∀ (X : Fin ((Opposite.unop n✝).len + 1)),
    (((functor (g.comp f)).map i j ≫ eqToHom ⋯).app n✝ a✝).obj X =
      (((EnrichedFunctor.comp SSet (functor f) (functor g)).map i j).app n✝ a✝).obj X

Tactic:
aesop_cat

Result:
no goals

Proof state:
case w.h
J K L : Type u
inst✝² : LinearOrder J
inst✝¹ : LinearOrder K
inst✝ : LinearOrder L
f : J →o K
g : K →o L
i j : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
a✝ : (EnrichedCategory.Hom i j).obj n✝
⊢ ((functor (g.comp f)).map i j ≫ eqToHom ⋯).app n✝ a✝ =
    ((EnrichedFunctor.comp SSet (functor f) (functor g)).map i j).app n✝ a✝

Tactic:
exact Functor.ext (by aesop_cat)

Result:
no goals

Proof state:
J K L : Type u
inst✝² : LinearOrder J
inst✝¹ : LinearOrder K
inst✝ : LinearOrder L
f : J →o K
g : K →o L
i j : SimplicialThickening J
⊢ (functor (g.comp f)).map i j ≫ eqToHom ⋯ = (EnrichedFunctor.comp SSet (functor f) (functor g)).map i j

Tactic:
ext

Result:
case w.h
J K L : Type u
inst✝² : LinearOrder J
inst✝¹ : LinearOrder K
inst✝ : LinearOrder L
f : J →o K
g : K →o L
i j : SimplicialThickening J
n✝ : SimplexCategoryᵒᵖ
a✝ : (EnrichedCategory.Hom i j).obj n✝
⊢ ((functor (g.comp f)).map i j ≫ eqToHom ⋯).app n✝ a✝ =
    ((EnrichedFunctor.comp SSet (functor f) (functor g)).map i j).app n✝ a✝
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive]
lemma orderOf_eq [Group G] (a : G) {x y : G} (h : SemiconjBy a x y) : orderOf x = orderOf y

Proof state:
G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
⊢ orderOf x = orderOf y

Tactic:
rw [orderOf_eq_orderOf_iff]

Result:
G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
⊢ ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1

Proof state:
G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
⊢ ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1

Tactic:
intro n

Result:
G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ x ^ n = 1 ↔ y ^ n = 1

Proof state:
G : Type u_1
inst✝ : Group G
a x y : G
h : SemiconjBy a x y
n : ℕ
⊢ x ^ n = 1 ↔ y ^ n = 1

Tactic:
exact (h.pow_right n).eq_one_iff

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma polyCharpoly_coeff_eq_zero_iff_of_basis (b : Basis ι R L) (b' : Basis ι' R L) (k : ℕ) :
    (polyCharpoly φ b).coeff k = 0 ↔ (polyCharpoly φ b').coeff k = 0

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
ι' : Type u_6
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : Fintype ι'
inst✝³ : DecidableEq ι
inst✝² : DecidableEq ι'
inst✝¹ : Free R M
inst✝ : Module.Finite R M
b : Basis ι R L
b' : Basis ι' R L
k : ℕ
⊢ (φ.polyCharpoly b).coeff k = 0 ↔ (φ.polyCharpoly b').coeff k = 0

Tactic:
constructor <;> apply polyCharpoly_coeff_eq_zero_of_basis

Result:
no goals
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma eq_rnDeriv_measure (h : κ = η.withDensity f + ξ)
    (hf : Measurable (Function.uncurry f)) (a : α) (hξ : ξ a ⟂ₘ η a) :
    f a =ᵐ[η a] ∂(κ a)/∂(η a)

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : ξ a ⟂ₘ η a
⊢ κ a = ξ a + (η a).withDensity (f a)

Tactic:
rw [h, coe_add, Pi.add_apply, η.withDensity_apply hf, add_comm]

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : ξ a ⟂ₘ η a
⊢ f a =ᶠ[ae (η a)] ∂κ a/∂η a

Tactic:
have : κ a = ξ a + (η a).withDensity (f a) := by
  rw [h, coe_add, Pi.add_apply, η.withDensity_apply hf, add_comm]

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : ξ a ⟂ₘ η a
this : κ a = ξ a + (η a).withDensity (f a)
⊢ f a =ᶠ[ae (η a)] ∂κ a/∂η a

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : ξ a ⟂ₘ η a
this : κ a = ξ a + (η a).withDensity (f a)
⊢ f a =ᶠ[ae (η a)] ∂κ a/∂η a

Tactic:
exact (κ a).eq_rnDeriv₀ (hf.comp measurable_prod_mk_left).aemeasurable hξ this

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem cramer_row_self (i : n) (h : ∀ j, b j = A j i) : A.cramer b = Pi.single i A.det

Proof state:
case h.e'_2.h.e'_6
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i : n
h : ∀ (j : n), b j = A j i
⊢ b = Aᵀ i

Tactic:
exact funext h

Result:
no goals

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i : n
h : ∀ (j : n), b j = A j i
⊢ Aᵀᵀ.cramer b = Pi.single i Aᵀ.det

Tactic:
convert cramer_transpose_row_self Aᵀ i

Result:
case h.e'_2.h.e'_6
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i : n
h : ∀ (j : n), b j = A j i
⊢ b = Aᵀ i

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i : n
h : ∀ (j : n), b j = A j i
⊢ A.cramer b = Pi.single i A.det

Tactic:
rw [← transpose_transpose A, det_transpose]

Result:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
i : n
h : ∀ (j : n), b j = A j i
⊢ Aᵀᵀ.cramer b = Pi.single i Aᵀ.det
-- Mathlib/Data/Matroid/Map.lean
lemma map_image_indep_iff {hf} {I : Set α} (hI : I ⊆ M.E) :
    (M.map f hf).Indep (f '' I) ↔ M.Indep I

Proof state:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
x✝ : ∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀
J : Set α
hJ : M.Indep J
hIJ : I = J
⊢ M.Indep I

Tactic:
rwa [hIJ]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
x✝ : ∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀
J : Set α
hJ : M.Indep J
hIJ : f '' I = f '' J
⊢ M.Indep I

Tactic:
rw [hf.image_eq_image_iff hI hJ.subset_ground] at hIJ

Result:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
x✝ : ∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀
J : Set α
hJ : M.Indep J
hIJ : I = J
⊢ M.Indep I

Proof state:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
⊢ (∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀) ↔ M.Indep I

Tactic:
refine ⟨fun ⟨J, hJ, hIJ⟩ ↦ ?_, fun h ↦ ⟨I, h, rfl⟩⟩

Result:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
x✝ : ∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀
J : Set α
hJ : M.Indep J
hIJ : f '' I = f '' J
⊢ M.Indep I

Proof state:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
⊢ (M.map f hf).Indep (f '' I) ↔ M.Indep I

Tactic:
rw [map_indep_iff]

Result:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
I : Set α
hI : I ⊆ M.E
⊢ (∃ I₀, M.Indep I₀ ∧ f '' I = f '' I₀) ↔ M.Indep I
-- Mathlib/Algebra/Order/Floor.lean
theorem fract_eq_fract {a b : α} : fract a = fract b ↔ ∃ z : ℤ, a - b = z :=
  ⟨fun h => ⟨⌊a⌋ - ⌊b⌋, by unfold fract at h; rw [Int.cast_sub, sub_eq_sub_iff_sub_eq_sub.1 h]⟩,
   by
    rintro ⟨z, hz⟩
    refine fract_eq_iff.2 ⟨fract_nonneg _, fract_lt_one _, z + ⌊b⌋, ?_⟩
    rw [eq_add_of_sub_eq hz, add_comm, Int.cast_add]
    exact add_sub_sub_cancel _ _ _⟩

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h : fract a = fract b
⊢ a - b = ↑(⌊a⌋ - ⌊b⌋)

Tactic:
unfold fract at h

Result:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h : a - ↑⌊a⌋ = b - ↑⌊b⌋
⊢ a - b = ↑(⌊a⌋ - ⌊b⌋)

Proof state:
case intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
z : ℤ
hz : a - b = ↑z
⊢ a - fract b = ↑(z + ⌊b⌋)

Tactic:
rw [eq_add_of_sub_eq hz, add_comm, Int.cast_add]

Result:
case intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
z : ℤ
hz : a - b = ↑z
⊢ b + ↑z - fract b = ↑z + ↑⌊b⌋

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ (∃ z, a - b = ↑z) → fract a = fract b

Tactic:
rintro ⟨z, hz⟩

Result:
case intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
z : ℤ
hz : a - b = ↑z
⊢ fract a = fract b

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
h : a - ↑⌊a⌋ = b - ↑⌊b⌋
⊢ a - b = ↑(⌊a⌋ - ⌊b⌋)

Tactic:
rw [Int.cast_sub, sub_eq_sub_iff_sub_eq_sub.1 h]

Result:
no goals

Proof state:
case intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
z : ℤ
hz : a - b = ↑z
⊢ fract a = fract b

Tactic:
refine fract_eq_iff.2 ⟨fract_nonneg _, fract_lt_one _, z + ⌊b⌋, ?_⟩

Result:
case intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
z : ℤ
hz : a - b = ↑z
⊢ a - fract b = ↑(z + ⌊b⌋)

Proof state:
case intro
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
z : ℤ
hz : a - b = ↑z
⊢ b + ↑z - fract b = ↑z + ↑⌊b⌋

Tactic:
exact add_sub_sub_cancel _ _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_cons' {x : BitVec w} :
    (cons a x).toNat = (a.toNat <<< w) + x.toNat

Proof state:
w : Nat
a : Bool
x : BitVec w
⊢ (cons a x).toNat = a.toNat <<< w + x.toNat

Tactic:
simp [cons, Nat.shiftLeft_eq, Nat.mul_comm _ (2^w), Nat.mul_add_lt_is_or, x.isLt]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem ord_univ : ord univ.{u, v} = Ordinal.univ.{u, v}

Proof state:
case intro
o✝ : Ordinal.{max (u + 1) v}
h : o✝ < Ordinal.univ.{u, v}
o : Ordinal.{u}
h' : liftPrincipalSeg.toRelEmbedding o = o✝
⊢ lift.{max (u + 1) v, u} o.card < univ.{u, v}

Tactic:
apply lift_lt_univ'

Result:
no goals

Proof state:
o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ.{u, v}
⊢ o.card < univ.{u, v}

Tactic:
have := liftPrincipalSeg.mem_range_of_rel_top (by simpa only [liftPrincipalSeg_coe] using h)

Result:
o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ.{u, v}
this : o ∈ range ⇑liftPrincipalSeg.toRelEmbedding
⊢ o.card < univ.{u, v}

Proof state:
o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ.{u, v}
this : o ∈ range ⇑liftPrincipalSeg.toRelEmbedding
⊢ o.card < univ.{u, v}

Tactic:
rcases this with ⟨o, h'⟩

Result:
case intro
o✝ : Ordinal.{max (u + 1) v}
h : o✝ < Ordinal.univ.{u, v}
o : Ordinal.{u}
h' : liftPrincipalSeg.toRelEmbedding o = o✝
⊢ o✝.card < univ.{u, v}

Proof state:
case intro
o✝ : Ordinal.{max (u + 1) v}
h : o✝ < Ordinal.univ.{u, v}
o : Ordinal.{u}
h' : liftPrincipalSeg.toRelEmbedding o = o✝
⊢ o✝.card < univ.{u, v}

Tactic:
rw [← h', liftPrincipalSeg_coe, ← lift_card]

Result:
case intro
o✝ : Ordinal.{max (u + 1) v}
h : o✝ < Ordinal.univ.{u, v}
o : Ordinal.{u}
h' : liftPrincipalSeg.toRelEmbedding o = o✝
⊢ lift.{max (u + 1) v, u} o.card < univ.{u, v}

Proof state:
⊢ univ.{u, v}.ord = Ordinal.univ.{u, v}

Tactic:
refine le_antisymm (ord_card_le _) <| le_of_forall_lt fun o h => lt_ord.2 ?_

Result:
o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ.{u, v}
⊢ o.card < univ.{u, v}

Proof state:
o : Ordinal.{max (u + 1) v}
h : o < Ordinal.univ.{u, v}
⊢ ?m.167211 < liftPrincipalSeg.top

Tactic:
simpa only [liftPrincipalSeg_coe] using h

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem eqToHom_unop {X Y : Cᵒᵖ} (h : X = Y) :
    (eqToHom h).unop = eqToHom (congr_arg unop h.symm)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
h : X = Y
⊢ (eqToHom h).unop = eqToHom ⋯

Tactic:
cases h

Result:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
⊢ (eqToHom ⋯).unop = eqToHom ⋯

Proof state:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : Cᵒᵖ
⊢ (eqToHom ⋯).unop = eqToHom ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem image_congr (h : (s : Set α).EqOn f g) : Finset.image f s = Finset.image g s

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g ↑s
a✝ : β
⊢ a✝ ∈ image f s ↔ a✝ ∈ image g s

Tactic:
simp_rw [mem_image, ← bex_def]

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g ↑s
a✝ : β
⊢ (∃ x, ∃ (_ : x ∈ s), f x = a✝) ↔ ∃ x, ∃ (_ : x ∈ s), g x = a✝

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g ↑s
a✝ : β
⊢ (∃ x, ∃ (_ : x ∈ s), f x = a✝) ↔ ∃ x, ∃ (_ : x ∈ s), g x = a✝

Tactic:
exact exists₂_congr fun x hx => by rw [h hx]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g ↑s
⊢ image f s = image g s

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g ↑s
a✝ : β
⊢ a✝ ∈ image f s ↔ a✝ ∈ image g s

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f g : α → β
s : Finset α
h : Set.EqOn f g ↑s
a✝ : β
x : α
hx : x ∈ s
⊢ f x = a✝ ↔ g x = a✝

Tactic:
rw [h hx]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean
theorem cs_down_0_not_rel_left (j : ℕ) : ¬c.Rel 0 j

Proof state:
j : ℕ
hj : j + 1 = 0
⊢ j.succ ≤ 0

Tactic:
rw [Nat.succ_eq_add_one, hj]

Result:
no goals

Proof state:
j : ℕ
⊢ ¬c.Rel 0 j

Tactic:
intro hj

Result:
j : ℕ
hj : c.Rel 0 j
⊢ False

Proof state:
j : ℕ
hj : c.Rel 0 j
⊢ False

Tactic:
dsimp at hj

Result:
j : ℕ
hj : j + 1 = 0
⊢ False

Proof state:
j : ℕ
hj : j + 1 = 0
⊢ False

Tactic:
apply Nat.not_succ_le_zero j

Result:
j : ℕ
hj : j + 1 = 0
⊢ j.succ ≤ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem idxOf?_eq_none_iff [BEq α] [LawfulBEq α] {l : Array α} {a : α} :
    l.idxOf? a = none ↔ a ∉ l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : Array α
a : α
⊢ l.idxOf? a = none ↔ ¬a ∈ l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ { toList := l }.idxOf? a = none ↔ ¬a ∈ { toList := l }

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ { toList := l }.idxOf? a = none ↔ ¬a ∈ { toList := l }

Tactic:
simp [List.idxOf?_eq_none_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
/-- When the function is over the base ring, the determinant is the evaluation at `1`. -/
@[simp] lemma det_ring (f : R →ₗ[R] R) : f.det = f 1

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R →ₗ[R] R
⊢ LinearMap.det f = f 1

Tactic:
simp [← det_toMatrix (Basis.singleton Unit R)]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma IsCircuit.finite [Finitary M] (hC : M.IsCircuit C) : C.Finite

Proof state:
α : Type u_1
M : Matroid α
C : Set α
inst✝ : M.Finitary
hC : M.IsCircuit C
hi : ¬M.Indep C
⊢ C.Finite

Tactic:
rw [indep_iff_forall_finite_subset_indep] at hi

Result:
α : Type u_1
M : Matroid α
C : Set α
inst✝ : M.Finitary
hC : M.IsCircuit C
hi : ¬∀ J ⊆ C, J.Finite → M.Indep J
⊢ C.Finite

Proof state:
α : Type u_1
M : Matroid α
C : Set α
inst✝ : M.Finitary
hC : M.IsCircuit C
⊢ C.Finite

Tactic:
have hi := hC.dep.not_indep

Result:
α : Type u_1
M : Matroid α
C : Set α
inst✝ : M.Finitary
hC : M.IsCircuit C
hi : ¬M.Indep C
⊢ C.Finite

Proof state:
case intro.intro.intro
α : Type u_1
M : Matroid α
C : Set α
inst✝ : M.Finitary
hC : M.IsCircuit C
J : Set α
hJC : J ⊆ C
hJfin : J.Finite
hJ : ¬M.Indep J
⊢ C.Finite

Tactic:
rwa [← hC.eq_of_not_indep_subset hJ hJC]

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
C : Set α
inst✝ : M.Finitary
hC : M.IsCircuit C
hi : ∃ J ⊆ C, J.Finite ∧ ¬M.Indep J
⊢ C.Finite

Tactic:
obtain ⟨J, hJC, hJfin, hJ⟩ := hi

Result:
case intro.intro.intro
α : Type u_1
M : Matroid α
C : Set α
inst✝ : M.Finitary
hC : M.IsCircuit C
J : Set α
hJC : J ⊆ C
hJfin : J.Finite
hJ : ¬M.Indep J
⊢ C.Finite

Proof state:
α : Type u_1
M : Matroid α
C : Set α
inst✝ : M.Finitary
hC : M.IsCircuit C
hi : ¬∀ J ⊆ C, J.Finite → M.Indep J
⊢ C.Finite

Tactic:
push_neg at hi

Result:
α : Type u_1
M : Matroid α
C : Set α
inst✝ : M.Finitary
hC : M.IsCircuit C
hi : ∃ J ⊆ C, J.Finite ∧ ¬M.Indep J
⊢ C.Finite
-- Mathlib/Topology/Connected/Basic.lean
theorem connectedComponentIn_mono (x : α) {F G : Set α} (h : F ⊆ G) :
    connectedComponentIn F x ⊆ connectedComponentIn G x

Proof state:
case neg
α : Type u
inst✝ : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∉ F
⊢ ∅ ⊆ connectedComponentIn G x

Tactic:
exact Set.empty_subset _

Result:
no goals

Proof state:
case pos
α : Type u
inst✝ : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∈ F
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x

Tactic:
rw [connectedComponentIn_eq_image hx, connectedComponentIn_eq_image (h hx), ←
  show ((↑) : G → α) ∘ inclusion h = (↑) from rfl, image_comp]

Result:
case pos
α : Type u
inst✝ : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∈ F
⊢ Subtype.val '' (inclusion h '' connectedComponent ⟨x, hx⟩) ⊆ Subtype.val '' connectedComponent ⟨x, ⋯⟩

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x

Tactic:
by_cases hx : x ∈ F

Result:
case pos
α : Type u
inst✝ : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∈ F
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x

case neg
α : Type u
inst✝ : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∉ F
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x

Proof state:
case neg
α : Type u
inst✝ : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∉ F
⊢ connectedComponentIn F x ⊆ connectedComponentIn G x

Tactic:
rw [connectedComponentIn_eq_empty hx]

Result:
case neg
α : Type u
inst✝ : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∉ F
⊢ ∅ ⊆ connectedComponentIn G x

Proof state:
case pos
α : Type u
inst✝ : TopologicalSpace α
x : α
F G : Set α
h : F ⊆ G
hx : x ∈ F
⊢ Subtype.val '' (inclusion h '' connectedComponent ⟨x, hx⟩) ⊆ Subtype.val '' connectedComponent ⟨x, ⋯⟩

Tactic:
exact image_subset _ ((continuous_inclusion h).image_connectedComponent_subset ⟨x, hx⟩)

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
theorem finsuppRight_apply (t : M ⊗[R] (ι →₀ N)) (i : ι) :
    finsuppRight R M N ι t i = lTensor M (Finsupp.lapply i) t

Proof state:
case add
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
i : ι
x y : M ⊗[R] (ι →₀ N)
hx : ((finsuppRight R M N ι) x) i = (lTensor M (Finsupp.lapply i)) x
hy : ((finsuppRight R M N ι) y) i = (lTensor M (Finsupp.lapply i)) y
⊢ ((finsuppRight R M N ι) (x + y)) i = (lTensor M (Finsupp.lapply i)) (x + y)

Tactic:
simp [map_add, hx, hy]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
t : M ⊗[R] (ι →₀ N)
i : ι
⊢ ((finsuppRight R M N ι) t) i = (lTensor M (Finsupp.lapply i)) t

Tactic:
induction t with
| zero => simp
| tmul m f => simp [finsuppRight_apply_tmul_apply]
| add x y hx hy => simp [map_add, hx, hy]

Result:
no goals

Proof state:
case tmul
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
i : ι
m : M
f : ι →₀ N
⊢ ((finsuppRight R M N ι) (m ⊗ₜ[R] f)) i = (lTensor M (Finsupp.lapply i)) (m ⊗ₜ[R] f)

Tactic:
simp [finsuppRight_apply_tmul_apply]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝⁵ : CommSemiring R
M : Type u_2
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
N : Type u_3
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_4
inst✝ : DecidableEq ι
i : ι
⊢ ((finsuppRight R M N ι) 0) i = (lTensor M (Finsupp.lapply i)) 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/PNat/Basic.lean
theorem le_sub_one_of_lt {a b : ℕ+} (hab : a < b) : a ≤ b - (1 : ℕ+)

Proof state:
case pos
a b : ℕ+
hab : a < b
h : 1 < b
⊢ ↑a ≤ ↑b - ↑1

Tactic:
exact Nat.le_pred_of_lt hab

Result:
no goals

Proof state:
a b : ℕ+
hab : a < b
⊢ a ≤ b - 1

Tactic:
rw [← coe_le_coe, sub_coe]

Result:
a b : ℕ+
hab : a < b
⊢ ↑a ≤ if 1 < b then ↑b - ↑1 else 1

Proof state:
case neg
a b : ℕ+
hab : a < b
h : ¬1 < b
⊢ ↑a ≤ 1

Tactic:
exact hab.le.trans (le_of_not_lt h)

Result:
no goals

Proof state:
a b : ℕ+
hab : a < b
⊢ ↑a ≤ if 1 < b then ↑b - ↑1 else 1

Tactic:
split_ifs with h

Result:
case pos
a b : ℕ+
hab : a < b
h : 1 < b
⊢ ↑a ≤ ↑b - ↑1

case neg
a b : ℕ+
hab : a < b
h : ¬1 < b
⊢ ↑a ≤ 1
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem degree_sum_eq_of_disjoint (f : S → R[X]) (s : Finset S)
    (h : Set.Pairwise { i | i ∈ s ∧ f i ≠ 0 } (Ne on degree ∘ f)) :
    degree (s.sum f) = s.sup fun i => degree (f i)

Proof state:
case insert.inr.inl.inr
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun i => (f i).degree
H : (f x).degree = (s.sum f).degree
hs : s.Nonempty
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree

Tactic:
obtain ⟨y, hy, hy'⟩ := Finset.exists_mem_eq_sup s hs fun i => degree (f i)

Result:
case insert.inr.inl.inr.intro.intro
R : Type u
S : Type v
inst✝ : Semiring R
f : S → R[X]
x : S
s : Finset S
hx : x ∉ s
h : {i | i ∈ insert x s ∧ f i ≠ 0}.Pairwise (Ne on degree ∘ f)
IH : (s.sum f).degree = s.sup fun i => (f i).degree
H : (f x).degree = (s.sum f).degree
hs : s.Nonempty
y : S
hy : y ∈ s
hy' : (s.sup fun i => (f i).degree) = (f y).degree
⊢ (f x + ∑ x ∈ s, f x).degree = (f x).degree ⊔ s.sup fun i => (f i).degree