harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Rotate.lean
theorem Nodup.rotate_congr_iff {l : List α} (hl : l.Nodup) {i j : ℕ} :
    l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []

Proof state:
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
⊢ l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []

Tactic:
rcases eq_or_ne l [] with rfl | hn

Result:
case inl
α : Type u
i j : ℕ
hl : [].Nodup
⊢ [].rotate i = [].rotate j ↔ i % [].length = j % [].length ∨ [] = []

case inr
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
⊢ l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []

Proof state:
case inr
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
⊢ l.rotate i = l.rotate j ↔ i % l.length = j % l.length

Tactic:
refine ⟨hl.rotate_congr hn _ _, fun h ↦ ?_⟩

Result:
case inr
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
h : i % l.length = j % l.length
⊢ l.rotate i = l.rotate j

Proof state:
case inr
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
⊢ l.rotate i = l.rotate j ↔ i % l.length = j % l.length ∨ l = []

Tactic:
simp only [hn, or_false]

Result:
case inr
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
⊢ l.rotate i = l.rotate j ↔ i % l.length = j % l.length

Proof state:
case inr
α : Type u
l : List α
hl : l.Nodup
i j : ℕ
hn : l ≠ []
h : i % l.length = j % l.length
⊢ l.rotate i = l.rotate j

Tactic:
rw [← rotate_mod, h, rotate_mod]

Result:
no goals

Proof state:
case inl
α : Type u
i j : ℕ
hl : [].Nodup
⊢ [].rotate i = [].rotate j ↔ i % [].length = j % [].length ∨ [] = []

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem sUnion_empty : ⋃₀ (∅ : ZFSet.{u}) = ∅

Proof state:
case a
z✝ : ZFSet.{u}
⊢ z✝ ∈ ⋃₀ ∅ ↔ z✝ ∈ ∅

Tactic:
simp

Result:
no goals

Proof state:
⊢ ⋃₀ ∅ = ∅

Tactic:
ext

Result:
case a
z✝ : ZFSet.{u}
⊢ z✝ ∈ ⋃₀ ∅ ↔ z✝ ∈ ∅
-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem mapRange.linearMap_comp (f : ∀ i, β₁ i →ₗ[R] β₂ i) (f₂ : ∀ i, β i →ₗ[R] β₁ i) :
    (mapRange.linearMap fun i => (f i).comp (f₂ i)) =
      (mapRange.linearMap f).comp (mapRange.linearMap f₂) :=
  LinearMap.ext <| mapRange_comp (fun i x => f i x) (fun i x => f₂ i x)
    (fun i => (f i).map_zero) (fun i => (f₂ i).map_zero) (by simp)

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁶ : Semiring R
β : ι → Type u_6
β₁ : ι → Type u_7
β₂ : ι → Type u_8
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (β₁ i)
inst✝³ : (i : ι) → AddCommMonoid (β₂ i)
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (β₁ i)
inst✝ : (i : ι) → Module R (β₂ i)
f : (i : ι) → β₁ i →ₗ[R] β₂ i
f₂ : (i : ι) → β i →ₗ[R] β₁ i
⊢ ∀ (i : ι), ((fun i x => (f i) x) i ∘ (fun i x => (f₂ i) x) i) 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
lemma of_fac' {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (ha : p.obj a = R) (hb : p.obj b = S)
    (h : p.map φ = eqToHom ha ≫ f ≫ eqToHom hb.symm) : p.IsHomLift f φ

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
h : p.map φ = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯
⊢ p.IsHomLift (p.map φ) φ

Tactic:
infer_instance

Result:
no goals

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
f : p.obj a ⟶ p.obj b
h : p.map φ = eqToHom ⋯ ≫ f ≫ eqToHom ⋯
⊢ p.IsHomLift f φ

Tactic:
obtain rfl : f = p.map φ := by simpa using h.symm

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
h : p.map φ = eqToHom ⋯ ≫ p.map φ ≫ eqToHom ⋯
⊢ p.IsHomLift (p.map φ) φ

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
f : p.obj a ⟶ p.obj b
h : p.map φ = eqToHom ⋯ ≫ f ≫ eqToHom ⋯
⊢ f = p.map φ

Tactic:
simpa using h.symm

Result:
no goals

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
R S : 𝒮
a b : 𝒳
f : R ⟶ S
φ : a ⟶ b
ha : p.obj a = R
hb : p.obj b = S
h : p.map φ = eqToHom ha ≫ f ≫ eqToHom ⋯
⊢ p.IsHomLift f φ

Tactic:
subst ha hb

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
φ : a ⟶ b
f : p.obj a ⟶ p.obj b
h : p.map φ = eqToHom ⋯ ≫ f ≫ eqToHom ⋯
⊢ p.IsHomLift f φ
-- Mathlib/GroupTheory/Nilpotent.lean
@[simp] lemma comap_upperCentralSeries {H : Type*} [Group H] (e : H ≃* G) :
    ∀ n, (upperCentralSeries G n).comap e = upperCentralSeries H n
  | 0 => by simpa [MonoidHom.ker_eq_bot_iff] using e.injective
  | n + 1 => by
    ext
    simp [mem_upperCentralSeries_succ_iff, ← comap_upperCentralSeries e n,
      ← e.toEquiv.forall_congr_right]

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : H ≃* G
⊢ comap (↑e) (upperCentralSeries G 0) = upperCentralSeries H 0

Tactic:
simpa [MonoidHom.ker_eq_bot_iff] using e.injective

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : H ≃* G
n : ℕ
⊢ comap (↑e) (upperCentralSeries G (n + 1)) = upperCentralSeries H (n + 1)

Tactic:
ext

Result:
case h
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : H ≃* G
n : ℕ
x✝ : H
⊢ x✝ ∈ comap (↑e) (upperCentralSeries G (n + 1)) ↔ x✝ ∈ upperCentralSeries H (n + 1)

Proof state:
case h
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : H ≃* G
n : ℕ
x✝ : H
⊢ x✝ ∈ comap (↑e) (upperCentralSeries G (n + 1)) ↔ x✝ ∈ upperCentralSeries H (n + 1)

Tactic:
simp [mem_upperCentralSeries_succ_iff, ← comap_upperCentralSeries e n,
  ← e.toEquiv.forall_congr_right]

Result:
no goals
-- Mathlib/RingTheory/FinitePresentation.lean
theorem mvPolynomial_of_finitePresentation [FinitePresentation.{w₁, w₂} R A]
    (ι : Type v) [Finite ι] :
    FinitePresentation.{w₁, max v w₂} R (MvPolynomial ι A)

Proof state:
case intro.intro.intro.intro.intro.refine_2
R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ⇑f
hf_ker : (RingHom.ker f.toRingHom).FG
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A := (MvPolynomial.mapAlgHom f).comp ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ (Ideal.map MvPolynomial.C (RingHom.ker ↑f)).FG

Tactic:
exact hf_ker.map MvPolynomial.C

Result:
no goals

Proof state:
R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
hfp : ∃ ι x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
⊢ ∃ ι_1 x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG

Tactic:
obtain ⟨(ι' : Type v), _, f, hf_surj, hf_ker⟩ := hfp

Result:
case intro.intro.intro.intro
R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ⇑f
hf_ker : (RingHom.ker f.toRingHom).FG
⊢ ∃ ι_1 x f, Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG

Proof state:
case intro.intro.intro.intro.intro.refine_1
R : Type w₁
A : Type w₂
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : FinitePresentation R A
ι : Type v
inst✝ : Finite ι
ι' : Type v
w✝ : Fintype ι'
f : MvPolynomial ι' R →ₐ[R] A
hf_surj : Surjective ⇑f
hf_ker : (RingHom.ker f.toRingHom).FG
g : MvPolynomial (ι ⊕ ι') R →ₐ[R] MvPolynomial ι A := (MvPolynomial.mapAlgHom f).comp ↑(MvPolynomial.sumAlgEquiv R ι ι')
val✝ : Fintype (ι ⊕ ι')
⊢ ⊥.FG

Tactic:
exact Submodule.fg_bot

Result:
no goals
-- Mathlib/Analysis/Normed/Module/FiniteDimension.lean
theorem continuous_clm_apply {X : Type*} [TopologicalSpace X] [FiniteDimensional 𝕜 E]
    {f : X → E →L[𝕜] F} : Continuous f ↔ ∀ y, Continuous (f · y)

Proof state:
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type v
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
F : Type w
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace 𝕜 F
inst✝² : CompleteSpace 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
⊢ Continuous f ↔ ∀ (y : E), Continuous fun x => (f x) y

Tactic:
simp_rw [continuous_iff_continuousOn_univ, continuousOn_clm_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_toArray (l : List (Array α)) :
    l.toArray.flatten = (l.map Array.toList).flatten.toArray

Proof state:
α : Type u_1
l : List (Array α)
⊢ l.toArray.flatten = (List.map toList l).flatten.toArray

Tactic:
apply ext'

Result:
case h
α : Type u_1
l : List (Array α)
⊢ l.toArray.flatten.toList = (List.map toList l).flatten.toArray.toList

Proof state:
case h
α : Type u_1
l : List (Array α)
⊢ l.toArray.flatten.toList = (List.map toList l).flatten.toArray.toList

Tactic:
simp

Result:
no goals
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem Directed.disjoint_iSup_right (h : Directed (· ≤ ·) f) :
    Disjoint a (⨆ i, f i) ↔ ∀ i, Disjoint a (f i)

Proof state:
ι : Sort u_1
α : Type u_2
inst✝¹ : CompleteLattice α
f : ι → α
inst✝ : IsCompactlyGenerated α
a : α
h : Directed (fun x1 x2 => x1 ≤ x2) f
⊢ Disjoint a (⨆ i, f i) ↔ ∀ (i : ι), Disjoint a (f i)

Tactic:
simp_rw [disjoint_iff, h.inf_iSup_eq, iSup_eq_bot]

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem mem_image : b ∈ s.image f ↔ ∃ a ∈ s, f a = b

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
f : α → β
s : Finset α
b : β
⊢ b ∈ image f s ↔ ∃ a ∈ s, f a = b

Tactic:
simp only [mem_def, image_val, mem_dedup, Multiset.mem_map, exists_prop]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean
theorem tangentBundle_model_space_coe_chartAt_symm (p : TangentBundle I H) :
    ((chartAt (ModelProd H E) p).symm : ModelProd H E → TangentBundle I H) =
      (TotalSpace.toProd H E).symm

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
⊢ ↑(chartAt (ModelProd H E) p).symm = ⇑(TotalSpace.toProd H E).symm

Tactic:
rw [← PartialHomeomorph.coe_coe, PartialHomeomorph.symm_toPartialEquiv,
  tangentBundle_model_space_chartAt]

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
⊢ ↑(TotalSpace.toProd H E).toPartialEquiv.symm = ⇑(TotalSpace.toProd H E).symm

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
H : Type u_4
inst✝ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
p : TangentBundle I H
⊢ ↑(TotalSpace.toProd H E).toPartialEquiv.symm = ⇑(TotalSpace.toProd H E).symm

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem pi_eq_empty_iff : s.pi t = ∅ ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
⊢ (∃ i, ∀ (x : α i), i ∈ s ∧ x ∉ t i) ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅

Tactic:
refine exists_congr fun i => ?_

Result:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
⊢ (∀ (x : α i), i ∈ s ∧ x ∉ t i) ↔ IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
⊢ s.pi t = ∅ ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅

Tactic:
rw [← not_nonempty_iff_eq_empty, pi_nonempty_iff]

Result:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
⊢ (¬∀ (i : ι), ∃ x, i ∈ s → x ∈ t i) ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
i : ι
⊢ (∀ (x : α i), i ∈ s ∧ x ∉ t i) ↔ IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅

Tactic:
cases isEmpty_or_nonempty (α i) <;> simp [*, forall_and, eq_empty_iff_forall_not_mem]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
⊢ (¬∀ (i : ι), ∃ x, i ∈ s → x ∈ t i) ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅

Tactic:
push_neg

Result:
ι : Type u_1
α : ι → Type u_2
s : Set ι
t : (i : ι) → Set (α i)
⊢ (∃ i, ∀ (x : α i), i ∈ s ∧ x ∉ t i) ↔ ∃ i, IsEmpty (α i) ∨ i ∈ s ∧ t i = ∅
-- Mathlib/Data/Finset/Card.lean
lemma injOn_of_surjOn_of_card_le (f : α → β) (hf : Set.MapsTo f s t) (hsurj : Set.SurjOn f s t)
    (hst : #s ≤ #t) : Set.InjOn f s

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
this✝¹ : image f s = t
this✝ : #(image f s) = #t
this : #(image f s) ≤ #s
⊢ Set.InjOn f ↑s

Tactic:
rw [← card_image_iff]

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
this✝¹ : image f s = t
this✝ : #(image f s) = #t
this : #(image f s) ≤ #s
⊢ #(image f s) = #s

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
this : image f s = t
⊢ #(image f s) = #t

Tactic:
rw [this]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
⊢ ↑(image f s) = ↑t

Tactic:
simp [hsurj.image_eq_of_mapsTo hf]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
this : image f s = t
⊢ Set.InjOn f ↑s

Tactic:
have : #(s.image f) = #t := by rw [this]

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
this✝ : image f s = t
this : #(image f s) = #t
⊢ Set.InjOn f ↑s

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
this✝ : image f s = t
this : #(image f s) = #t
⊢ Set.InjOn f ↑s

Tactic:
have : #(s.image f) ≤ #s := card_image_le

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
this✝¹ : image f s = t
this✝ : #(image f s) = #t
this : #(image f s) ≤ #s
⊢ Set.InjOn f ↑s

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
⊢ Set.InjOn f ↑s

Tactic:
classical
have : s.image f = t := Finset.coe_injective <| by simp [hsurj.image_eq_of_mapsTo hf]
have : #(s.image f) = #t := by rw [this]
have : #(s.image f) ≤ #s := card_image_le
rw [← card_image_iff]
omega

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
⊢ Set.InjOn f ↑s

Tactic:
have : s.image f = t := Finset.coe_injective <| by simp [hsurj.image_eq_of_mapsTo hf]

Result:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
this : image f s = t
⊢ Set.InjOn f ↑s

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α → β
hf : Set.MapsTo f ↑s ↑t
hsurj : Set.SurjOn f ↑s ↑t
hst : #s ≤ #t
this✝¹ : image f s = t
this✝ : #(image f s) = #t
this : #(image f s) ≤ #s
⊢ #(image f s) = #s

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/Sites/MayerVietorisSquare.lean
lemma bijective_toPullbackObj : Function.Bijective (S.toPullbackObj P)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : HasWeakSheafify J (Type v)
S : J.MayerVietorisSquare
P : Cᵒᵖ ⥤ Type v'
h : S.SheafCondition P
⊢ Function.Bijective (S.toPullbackObj P)

Tactic:
rwa [← sheafCondition_iff_bijective_toPullbackObj]

Result:
no goals
-- Mathlib/Data/List/Perm/Lattice.lean
theorem Perm.dropSlice_inter {xs ys : List α} (n m : ℕ) (h : xs ~ ys)
    (h' : ys.Nodup) : List.dropSlice n m xs ~ ys ∩ List.dropSlice n m xs

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
h₂ : xs.Nodup
⊢ take n xs ++ drop (n + m) xs ~ ys ∩ take n xs ++ ys ∩ drop (n + m) xs

Tactic:
exact Perm.append (Perm.take_inter _ h h') (Perm.drop_inter _ h h')

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ take n xs ++ drop (n + m) xs ~ ys ∩ (take n xs ++ drop (n + m) xs)

Tactic:
have : n ≤ n + m := Nat.le_add_right _ _

Result:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
⊢ take n xs ++ drop (n + m) xs ~ ys ∩ (take n xs ++ drop (n + m) xs)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
h₂ : xs.Nodup
⊢ (take n xs).Disjoint (drop (n + m) xs)

Tactic:
exact disjoint_take_drop h₂ this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
h₂ : xs.Nodup
⊢ take n xs ++ drop (n + m) xs ~ ys ∩ (take n xs ++ drop (n + m) xs)

Tactic:
apply Perm.trans _ (Perm.inter_append _).symm

Result:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
h₂ : xs.Nodup
⊢ take n xs ++ drop (n + m) xs ~ ys ∩ take n xs ++ ys ∩ drop (n + m) xs

α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
h₂ : xs.Nodup
⊢ (take n xs).Disjoint (drop (n + m) xs)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ dropSlice n m xs ~ ys ∩ dropSlice n m xs

Tactic:
simp only [dropSlice_eq]

Result:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ take n xs ++ drop (n + m) xs ~ ys ∩ (take n xs ++ drop (n + m) xs)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
⊢ take n xs ++ drop (n + m) xs ~ ys ∩ (take n xs ++ drop (n + m) xs)

Tactic:
have h₂ := h.nodup_iff.2 h'

Result:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : ys.Nodup
this : n ≤ n + m
h₂ : xs.Nodup
⊢ take n xs ++ drop (n + m) xs ~ ys ∩ (take n xs ++ drop (n + m) xs)
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem basisSets_zero (U) (hU : U ∈ p.basisSets) : (0 : E) ∈ U

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ p.basisSets
ι' : Finset ι
r : ℝ
hr : 0 < r
hU : U = (ι'.sup p).ball 0 r
⊢ 0 < r

Tactic:
exact hr

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU : U ∈ p.basisSets
⊢ 0 ∈ U

Tactic:
rcases p.basisSets_iff.mp hU with ⟨ι', r, hr, hU⟩

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ p.basisSets
ι' : Finset ι
r : ℝ
hr : 0 < r
hU : U = (ι'.sup p).ball 0 r
⊢ 0 ∈ U

Proof state:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ p.basisSets
ι' : Finset ι
r : ℝ
hr : 0 < r
hU : U = (ι'.sup p).ball 0 r
⊢ 0 ∈ U

Tactic:
rw [hU, mem_ball_zero, map_zero]

Result:
case intro.intro.intro
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : SeminormFamily 𝕜 E ι
U : Set E
hU✝ : U ∈ p.basisSets
ι' : Finset ι
r : ℝ
hr : 0 < r
hU : U = (ι'.sup p).ball 0 r
⊢ 0 < r
-- Mathlib/AlgebraicGeometry/Stalk.lean
@[reassoc (attr := simp)]
lemma germ_stalkClosedPointIso_hom :
    (Spec R).presheaf.germ ⊤ (closedPoint _) trivial ≫ (stalkClosedPointIso R).hom =
      (Scheme.ΓSpecIso R).hom

Proof state:
R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ (Spec R).presheaf.germ ⊤ (closedPoint ↑R) trivial ≫ (stalkClosedPointIso R).hom = (Scheme.ΓSpecIso R).hom

Tactic:
rw [← ΓSpecIso_hom_stalkClosedPointIso_inv, Category.assoc, Iso.inv_hom_id, Category.comp_id]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Division.lean
theorem mul_of'_modOf (x : k[G]) (g : G) : x * of' k G g %ᵒᶠ g = 0

Proof state:
case H.inr.h
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ ¬∃ d, g' = d + g

Tactic:
simpa only [add_comm] using h

Result:
no goals

Proof state:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
⊢ (x * of' k G g %ᵒᶠ g) g' = 0 g'

Tactic:
rw [Finsupp.zero_apply]

Result:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
⊢ (x * of' k G g %ᵒᶠ g) g' = 0

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g : G
⊢ x * of' k G g %ᵒᶠ g = 0

Tactic:
ext g'

Result:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
⊢ (x * of' k G g %ᵒᶠ g) g' = 0 g'

Proof state:
case H.inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (x * of' k G g %ᵒᶠ g) g' = 0

Tactic:
rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, mul_single_apply_of_not_exists_add]

Result:
case H.inr.h
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ ¬∃ d, g' = d + g

Proof state:
case H.inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g d : G
⊢ (x * of' k G g %ᵒᶠ g) (g + d) = 0

Tactic:
rw [modOf_apply_self_add]

Result:
no goals

Proof state:
case H
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
⊢ (x * of' k G g %ᵒᶠ g) g' = 0

Tactic:
obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d)

Result:
case H.inl.intro
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g d : G
⊢ (x * of' k G g %ᵒᶠ g) (g + d) = 0

case H.inr
k : Type u_1
G : Type u_2
inst✝¹ : Semiring k
inst✝ : AddCancelCommMonoid G
x : k[G]
g g' : G
h : ¬∃ d, g' = g + d
⊢ (x * of' k G g %ᵒᶠ g) g' = 0
-- Mathlib/LinearAlgebra/Matrix/DotProduct.lean
lemma conjTranspose_mul_self_mul_eq_zero {p} (A : Matrix m n R) (B : Matrix n p R) :
    (Aᴴ * A) * B = 0 ↔ A * B = 0

Proof state:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
p : Type u_5
A : Matrix m n R
B : Matrix n p R
h : A * B = 0
⊢ Aᴴ * A * B = 0

Tactic:
simp only [Matrix.mul_assoc, h, Matrix.mul_zero]

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
p : Type u_5
A : Matrix m n R
B : Matrix n p R
⊢ Aᴴ * A * B = 0 ↔ A * B = 0

Tactic:
refine ⟨fun h => ?_, fun h => by simp only [Matrix.mul_assoc, h, Matrix.mul_zero]⟩

Result:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
p : Type u_5
A : Matrix m n R
B : Matrix n p R
h : Aᴴ * A * B = 0
⊢ A * B = 0

Proof state:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
p : Type u_5
A : Matrix m n R
B : Matrix n p R
h : Bᴴ * (Aᴴ * A * B) = Bᴴ * 0
⊢ A * B = 0

Tactic:
rwa [Matrix.mul_zero, Matrix.mul_assoc, ← Matrix.mul_assoc, ← conjTranspose_mul,
  conjTranspose_mul_self_eq_zero] at h

Result:
no goals