harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem linearIndependent_unique_iff (v : ι → M) [Unique ι] :
    LinearIndependent R v ↔ v default ≠ 0

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
v : ι → M
inst✝ : Unique ι
⊢ (∀ (l : ι →₀ R), l default = 0 ∨ v default = 0 → l = 0) ↔ v default ≠ 0

Tactic:
refine ⟨fun h hv => ?_, fun hv l hl => Finsupp.unique_ext <| hl.resolve_right hv⟩

Result:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
v : ι → M
inst✝ : Unique ι
h : ∀ (l : ι →₀ R), l default = 0 ∨ v default = 0 → l = 0
hv : v default = 0
⊢ False

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
v : ι → M
inst✝ : Unique ι
h : ∀ (l : ι →₀ R), l default = 0 ∨ v default = 0 → l = 0
hv : v default = 0
⊢ False

Tactic:
have := h (Finsupp.single default 1) (Or.inr hv)

Result:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
v : ι → M
inst✝ : Unique ι
h : ∀ (l : ι →₀ R), l default = 0 ∨ v default = 0 → l = 0
hv : v default = 0
this : Finsupp.single default 1 = 0
⊢ False

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
v : ι → M
inst✝ : Unique ι
h : ∀ (l : ι →₀ R), l default = 0 ∨ v default = 0 → l = 0
hv : v default = 0
this : Finsupp.single default 1 = 0
⊢ False

Tactic:
exact one_ne_zero (Finsupp.single_eq_zero.1 this)

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
v : ι → M
inst✝ : Unique ι
⊢ LinearIndependent R v ↔ v default ≠ 0

Tactic:
simp only [linearIndependent_iff, Finsupp.linearCombination_unique, smul_eq_zero]

Result:
ι : Type u'
R : Type u_2
M : Type u_4
inst✝⁵ : Ring R
inst✝⁴ : Nontrivial R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : NoZeroSMulDivisors R M
v : ι → M
inst✝ : Unique ι
⊢ (∀ (l : ι →₀ R), l default = 0 ∨ v default = 0 → l = 0) ↔ v default ≠ 0
-- Mathlib/Order/PartialSups.lean
theorem ciSup_partialSups_eq [ConditionallyCompleteLattice α]
    {f : ι → α} (h : BddAbove (Set.range f)) :
    ⨆ i, partialSups f i = ⨆ i, f i

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
by_cases hι : Nonempty ι

Result:
case pos
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

case neg
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : ¬Nonempty ι
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Proof state:
case pos
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
refine (ciSup_le fun i ↦ ?_).antisymm (ciSup_mono ?_ <| le_partialSups f)

Result:
case pos.refine_1
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
i : ι
⊢ (partialSups f) i ≤ ⨆ i, f i

case pos.refine_2
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ BddAbove (Set.range fun i => (partialSups f) i)

Proof state:
case pos.refine_1
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
i : ι
⊢ (partialSups f) i ≤ ⨆ i, f i

Tactic:
simpa only [partialSups_eq_ciSup_Iic] using ciSup_le fun i ↦ le_ciSup h _

Result:
no goals

Proof state:
case neg
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : ¬Nonempty ι
⊢ ⨆ i, (partialSups f) i = ⨆ i, f i

Tactic:
exact congr_arg _ (funext (not_nonempty_iff.mp hι).elim)

Result:
no goals

Proof state:
case pos.refine_2
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : ConditionallyCompleteLattice α
f : ι → α
h : BddAbove (Set.range f)
hι : Nonempty ι
⊢ BddAbove (Set.range fun i => (partialSups f) i)

Tactic:
rwa [bddAbove_range_partialSups]

Result:
no goals
-- Mathlib/Order/Basic.lean
theorem lt_iff : x < y ↔ x.1 < y.1 ∧ x.2 ≤ y.2 ∨ x.1 ≤ y.1 ∧ x.2 < y.2

Proof state:
case refine_2.inl.intro
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst < y.fst
h₂ : x.snd ≤ y.snd
⊢ x < y

Tactic:
exact ⟨⟨h₁.le, h₂⟩, fun h ↦ h₁.not_le h.1⟩

Result:
no goals

Proof state:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h : x < y
h₁ : y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
exact Or.inr ⟨h.1.1, LE.le.lt_of_not_le h.1.2 fun h₂ ↦ h.2 ⟨h₁, h₂⟩⟩

Result:
no goals

Proof state:
case neg
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h : x < y
h₁ : ¬y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
exact Or.inl ⟨LE.le.lt_of_not_le h.1.1 h₁, h.1.2⟩

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
⊢ x < y ↔ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Result:
case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h : x < y
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd → x < y

Proof state:
case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h : x < y
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Tactic:
by_cases h₁ : y.1 ≤ x.1

Result:
case pos
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h : x < y
h₁ : y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

case neg
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h : x < y
h₁ : ¬y.fst ≤ x.fst
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd

Proof state:
case refine_2.inr.intro
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y

Tactic:
exact ⟨⟨h₁, h₂.le⟩, fun h ↦ h₂.not_le h.2⟩

Result:
no goals

Proof state:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd → x < y

Tactic:
rintro (⟨h₁, h₂⟩ | ⟨h₁, h₂⟩)

Result:
case refine_2.inl.intro
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst < y.fst
h₂ : x.snd ≤ y.snd
⊢ x < y

case refine_2.inr.intro
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
x y : α × β
h₁ : x.fst ≤ y.fst
h₂ : x.snd < y.snd
⊢ x < y
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma map_sub : (z - z').map Φ = z.map Φ - z'.map Φ

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
D : Type u_2
inst✝² : Category.{u_3, u_2} D
inst✝¹ : Preadditive D
z z' : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
⊢ (z - z').map Φ = z.map Φ - z'.map Φ

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
/-- The `changeLevel` map is injective (except in the degenerate case `m = 0`). -/
lemma changeLevel_injective {m : ℕ} [NeZero m] (hm : n ∣ m) :
    Function.Injective (changeLevel (R := R) hm)

Proof state:
case h
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n m : ℕ
inst✝ : NeZero m
hm : n ∣ m
a₁✝ a₂✝ : DirichletCharacter R n
h : (changeLevel hm) a₁✝ = (changeLevel hm) a₂✝
y : (ZMod n)ˣ
⊢ a₁✝ ↑y = a₂✝ ↑y

Tactic:
obtain ⟨z, rfl⟩ := ZMod.unitsMap_surjective hm y

Result:
case h.intro
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n m : ℕ
inst✝ : NeZero m
hm : n ∣ m
a₁✝ a₂✝ : DirichletCharacter R n
h : (changeLevel hm) a₁✝ = (changeLevel hm) a₂✝
z : (ZMod m)ˣ
⊢ a₁✝ ↑((ZMod.unitsMap hm) z) = a₂✝ ↑((ZMod.unitsMap hm) z)

Proof state:
case h.intro
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n m : ℕ
inst✝ : NeZero m
hm : n ∣ m
a₁✝ a₂✝ : DirichletCharacter R n
h : ∀ (a : (ZMod m)ˣ), ((changeLevel hm) a₁✝) ↑a = ((changeLevel hm) a₂✝) ↑a
z : (ZMod m)ˣ
⊢ a₁✝ ↑((ZMod.unitsMap hm) z) = a₂✝ ↑((ZMod.unitsMap hm) z)

Tactic:
simpa [changeLevel_def] using h z

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n m : ℕ
inst✝ : NeZero m
hm : n ∣ m
a₁✝ a₂✝ : DirichletCharacter R n
h : (changeLevel hm) a₁✝ = (changeLevel hm) a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext1 y

Result:
case h
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n m : ℕ
inst✝ : NeZero m
hm : n ∣ m
a₁✝ a₂✝ : DirichletCharacter R n
h : (changeLevel hm) a₁✝ = (changeLevel hm) a₂✝
y : (ZMod n)ˣ
⊢ a₁✝ ↑y = a₂✝ ↑y

Proof state:
case h.intro
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n m : ℕ
inst✝ : NeZero m
hm : n ∣ m
a₁✝ a₂✝ : DirichletCharacter R n
h : (changeLevel hm) a₁✝ = (changeLevel hm) a₂✝
z : (ZMod m)ˣ
⊢ a₁✝ ↑((ZMod.unitsMap hm) z) = a₂✝ ↑((ZMod.unitsMap hm) z)

Tactic:
rw [MulChar.ext_iff] at h

Result:
case h.intro
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n m : ℕ
inst✝ : NeZero m
hm : n ∣ m
a₁✝ a₂✝ : DirichletCharacter R n
h : ∀ (a : (ZMod m)ˣ), ((changeLevel hm) a₁✝) ↑a = ((changeLevel hm) a₂✝) ↑a
z : (ZMod m)ˣ
⊢ a₁✝ ↑((ZMod.unitsMap hm) z) = a₂✝ ↑((ZMod.unitsMap hm) z)

Proof state:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n m : ℕ
inst✝ : NeZero m
hm : n ∣ m
⊢ Function.Injective ⇑(changeLevel hm)

Tactic:
intro _ _ h

Result:
R : Type u_1
inst✝¹ : CommMonoidWithZero R
n m : ℕ
inst✝ : NeZero m
hm : n ∣ m
a₁✝ a₂✝ : DirichletCharacter R n
h : (changeLevel hm) a₁✝ = (changeLevel hm) a₂✝
⊢ a₁✝ = a₂✝
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem Irreducible.natDegree_pos {F : Type*} [Field F] {f : F[X]} (h : Irreducible f) :
    0 < f.natDegree := Nat.pos_of_ne_zero fun H ↦ by
  obtain ⟨x, hf⟩ := natDegree_eq_zero.1 H
  by_cases hx : x = 0
  · rw [← hf, hx, map_zero] at h; exact not_irreducible_zero h
  exact h.1 (hf ▸ isUnit_C.2 (Ne.isUnit hx))

Proof state:
case neg
F : Type u_1
inst✝ : Field F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : C x = f
hx : ¬x = 0
⊢ False

Tactic:
exact h.1 (hf ▸ isUnit_C.2 (Ne.isUnit hx))

Result:
no goals

Proof state:
F : Type u_1
inst✝ : Field F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
⊢ False

Tactic:
obtain ⟨x, hf⟩ := natDegree_eq_zero.1 H

Result:
case intro
F : Type u_1
inst✝ : Field F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : C x = f
⊢ False

Proof state:
case pos
F : Type u_1
inst✝ : Field F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : C x = f
hx : x = 0
⊢ False

Tactic:
rw [← hf, hx, map_zero] at h

Result:
case pos
F : Type u_1
inst✝ : Field F
f : F[X]
H : f.natDegree = 0
x : F
h : Irreducible 0
hf : C x = f
hx : x = 0
⊢ False

Proof state:
case pos
F : Type u_1
inst✝ : Field F
f : F[X]
H : f.natDegree = 0
x : F
h : Irreducible 0
hf : C x = f
hx : x = 0
⊢ False

Tactic:
exact not_irreducible_zero h

Result:
no goals

Proof state:
case intro
F : Type u_1
inst✝ : Field F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : C x = f
⊢ False

Tactic:
by_cases hx : x = 0

Result:
case pos
F : Type u_1
inst✝ : Field F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : C x = f
hx : x = 0
⊢ False

case neg
F : Type u_1
inst✝ : Field F
f : F[X]
h : Irreducible f
H : f.natDegree = 0
x : F
hf : C x = f
hx : ¬x = 0
⊢ False
-- Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
theorem toFun_unique (g : L ≃+* L) (c : ZMod (Fintype.card (rootsOfUnity n L)))
    (hc : ∀ t : rootsOfUnity n L, g (t : Lˣ) = (t ^ c.val : Lˣ)) : c = χ₀ n g

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card ↥(rootsOfUnity n L))
ζ : ↥(rootsOfUnity n L)
hc : g ↑↑ζ = ↑(↑ζ ^ c.val)
⊢ ↑(↑ζ ^ c.val) = ↑(↑ζ ^ (χ₀ n g).val)

Tactic:
rw [← toFun_spec g ζ, hc]

Result:
no goals

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card ↥(rootsOfUnity n L))
ζ : ↥(rootsOfUnity n L)
hc : g ↑↑ζ = ↑(↑ζ ^ c.val)
this : ↑(↑ζ ^ c.val) = ↑(↑ζ ^ (χ₀ n g).val)
⊢ ζ ^ c.val = ζ ^ (χ₀ n g).val

Tactic:
exact_mod_cast this

Result:
no goals

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card ↥(rootsOfUnity n L))
ζ : ↥(rootsOfUnity n L)
hc : g ↑↑ζ = ↑(↑ζ ^ c.val)
⊢ ζ ^ c.val = ζ ^ (χ₀ n g).val

Tactic:
suffices ((ζ ^ c.val : Lˣ) : L) = (ζ ^ (χ₀ n g).val : Lˣ) by exact_mod_cast this

Result:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card ↥(rootsOfUnity n L))
ζ : ↥(rootsOfUnity n L)
hc : g ↑↑ζ = ↑(↑ζ ^ c.val)
⊢ ↑(↑ζ ^ c.val) = ↑(↑ζ ^ (χ₀ n g).val)

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card ↥(rootsOfUnity n L))
hc : ∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ c.val)
ζ : ↥(rootsOfUnity n L)
⊢ ζ ^ c.val = ζ ^ (χ₀ n g).val

Tactic:
specialize hc ζ

Result:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card ↥(rootsOfUnity n L))
ζ : ↥(rootsOfUnity n L)
hc : g ↑↑ζ = ↑(↑ζ ^ c.val)
⊢ ζ ^ c.val = ζ ^ (χ₀ n g).val

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card ↥(rootsOfUnity n L))
hc : ∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ c.val)
⊢ c = χ₀ n g

Tactic:
apply IsCyclic.ext Nat.card_eq_fintype_card (fun ζ ↦ ?_)

Result:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
g : L ≃+* L
c : ZMod (Fintype.card ↥(rootsOfUnity n L))
hc : ∀ (t : ↥(rootsOfUnity n L)), g ↑↑t = ↑(↑t ^ c.val)
ζ : ↥(rootsOfUnity n L)
⊢ ζ ^ c.val = ζ ^ (χ₀ n g).val
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem two_le_of_mem_cycleType {σ : Perm α} {n : ℕ} (h : n ∈ σ.cycleType) : 2 ≤ n

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ w✝ : Perm α
hc : w✝.IsCycle
⊢ 2 ≤ w✝.support.card

Tactic:
exact hc.two_le_card_support

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : n ∈ σ.cycleType
⊢ 2 ≤ n

Tactic:
simp only [cycleType_def, ← Finset.mem_def, Function.comp_apply, Multiset.mem_map,
  mem_cycleFactorsFinset_iff] at h

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : ∃ a, (a.IsCycle ∧ ∀ a_1 ∈ a.support, a a_1 = σ a_1) ∧ a.support.card = n
⊢ 2 ≤ n

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
n : ℕ
h : ∃ a, (a.IsCycle ∧ ∀ a_1 ∈ a.support, a a_1 = σ a_1) ∧ a.support.card = n
⊢ 2 ≤ n

Tactic:
obtain ⟨_, ⟨hc, -⟩, rfl⟩ := h

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ w✝ : Perm α
hc : w✝.IsCycle
⊢ 2 ≤ w✝.support.card
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem mem_graph_iff' (f : E →ₗ.[R] F) {x : E × F} :
    x ∈ f.graph ↔ ∃ y : f.domain, (↑y, f y) = x

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x : E × F
⊢ x ∈ f.graph ↔ ∃ y, (↑y, ↑f y) = x

Tactic:
simp [graph]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem finrank_vectorSpan_range_le [Fintype ι] (p : ι → P) {n : ℕ} (hc : Fintype.card ι = n + 1) :
    finrank k (vectorSpan k (Set.range p)) ≤ n

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k ↥(vectorSpan k (Set.range p)) ≤ n

Tactic:
classical
rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image]
rw [← Finset.card_univ] at hc
exact finrank_vectorSpan_image_finset_le _ _ _ hc

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k ↥(vectorSpan k ↑(Finset.image p Finset.univ)) ≤ n

Tactic:
rw [← Finset.card_univ] at hc

Result:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : #Finset.univ = n + 1
⊢ finrank k ↥(vectorSpan k ↑(Finset.image p Finset.univ)) ≤ n

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k ↥(vectorSpan k (Set.range p)) ≤ n

Tactic:
rw [← Set.image_univ, ← Finset.coe_univ, ← Finset.coe_image]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : Fintype.card ι = n + 1
⊢ finrank k ↥(vectorSpan k ↑(Finset.image p Finset.univ)) ≤ n

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
ι : Type u_4
inst✝⁴ : DivisionRing k
inst✝³ : AddCommGroup V
inst✝² : Module k V
inst✝¹ : AffineSpace V P
inst✝ : Fintype ι
p : ι → P
n : ℕ
hc : #Finset.univ = n + 1
⊢ finrank k ↥(vectorSpan k ↑(Finset.image p Finset.univ)) ≤ n

Tactic:
exact finrank_vectorSpan_image_finset_le _ _ _ hc

Result:
no goals
-- Mathlib/RingTheory/Nullstellensatz.lean
theorem radical_le_vanishingIdeal_zeroLocus (I : Ideal (MvPolynomial σ k)) :
    I.radical ≤ vanishingIdeal (zeroLocus I)

Proof state:
k : Type u_1
inst✝ : Field k
σ : Type u_2
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ I.radical
x : σ → k
hx : x ∈ zeroLocus I
⊢ (eval x) p = 0

Tactic:
rw [← mem_vanishingIdeal_singleton_iff]

Result:
k : Type u_1
inst✝ : Field k
σ : Type u_2
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ I.radical
x : σ → k
hx : x ∈ zeroLocus I
⊢ p ∈ vanishingIdeal {x}

Proof state:
k : Type u_1
inst✝ : Field k
σ : Type u_2
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ sInf {J | I ≤ J ∧ J.IsPrime}
x : σ → k
hx : x ∈ zeroLocus I
⊢ p ∈ vanishingIdeal {x}

Tactic:
refine
  (mem_sInf.mp hp)
    ⟨le_trans (le_vanishingIdeal_zeroLocus I)
        (vanishingIdeal_anti_mono fun y hy => hy.symm ▸ hx),
      IsMaximal.isPrime' _⟩

Result:
no goals

Proof state:
k : Type u_1
inst✝ : Field k
σ : Type u_2
I : Ideal (MvPolynomial σ k)
⊢ I.radical ≤ vanishingIdeal (zeroLocus I)

Tactic:
intro p hp x hx

Result:
k : Type u_1
inst✝ : Field k
σ : Type u_2
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ I.radical
x : σ → k
hx : x ∈ zeroLocus I
⊢ (eval x) p = 0

Proof state:
k : Type u_1
inst✝ : Field k
σ : Type u_2
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ I.radical
x : σ → k
hx : x ∈ zeroLocus I
⊢ p ∈ vanishingIdeal {x}

Tactic:
rw [radical_eq_sInf] at hp

Result:
k : Type u_1
inst✝ : Field k
σ : Type u_2
I : Ideal (MvPolynomial σ k)
p : MvPolynomial σ k
hp : p ∈ sInf {J | I ≤ J ∧ J.IsPrime}
x : σ → k
hx : x ∈ zeroLocus I
⊢ p ∈ vanishingIdeal {x}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem foldlM_attachWith [Monad m]
    (l : Array α) {q : α → Prop} (H : ∀ a, a ∈ l → q a) {f : β → { x // q x} → m β} {b} (w : stop = l.size):
    (l.attachWith q H).foldlM f b 0 stop =
      l.attach.foldlM (fun b ⟨a, h⟩ => f b ⟨a, H _ h⟩) b

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
l : Array α
q : α → Prop
H : ∀ (a : α), a ∈ l → q a
f : β → { x // q x } → m β
b : β
⊢ foldlM f b (l.attachWith q H) 0 l.size =
    foldlM
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
      b l.attach

Tactic:
rcases l with ⟨l⟩

Result:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
q : α → Prop
f : β → { x // q x } → m β
b : β
l : List α
H : ∀ (a : α), a ∈ { toList := l } → q a
⊢ foldlM f b ({ toList := l }.attachWith q H) 0 { toList := l }.size =
    foldlM
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
      b { toList := l }.attach

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
stop : Nat
inst✝ : Monad m
l : Array α
q : α → Prop
H : ∀ (a : α), a ∈ l → q a
f : β → { x // q x } → m β
b : β
w : stop = l.size
⊢ foldlM f b (l.attachWith q H) 0 stop =
    foldlM
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
      b l.attach

Tactic:
subst w

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
l : Array α
q : α → Prop
H : ∀ (a : α), a ∈ l → q a
f : β → { x // q x } → m β
b : β
⊢ foldlM f b (l.attachWith q H) 0 l.size =
    foldlM
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
      b l.attach

Proof state:
case mk
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝ : Monad m
q : α → Prop
f : β → { x // q x } → m β
b : β
l : List α
H : ∀ (a : α), a ∈ { toList := l } → q a
⊢ foldlM f b ({ toList := l }.attachWith q H) 0 { toList := l }.size =
    foldlM
      (fun b x =>
        match x with
        | ⟨a, h⟩ => f b ⟨a, ⋯⟩)
      b { toList := l }.attach

Tactic:
simp [List.foldlM_map]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem lowerClosure_image (f : α ≃o β) :
    lowerClosure (f '' s) = LowerSet.map f (lowerClosure s)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
⊢ lowerClosure (⇑f '' s) = (LowerSet.map f.symm).symm (lowerClosure s)

Tactic:
ext

Result:
case a.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
x✝ : β
⊢ x✝ ∈ ↑(lowerClosure (⇑f '' s)) ↔ x✝ ∈ ↑((LowerSet.map f.symm).symm (lowerClosure s))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
⊢ lowerClosure (⇑f '' s) = (LowerSet.map f) (lowerClosure s)

Tactic:
rw [← f.symm_symm, ← LowerSet.symm_map, f.symm_symm]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
⊢ lowerClosure (⇑f '' s) = (LowerSet.map f.symm).symm (lowerClosure s)

Proof state:
case a.h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
f : α ≃o β
x✝ : β
⊢ x✝ ∈ ↑(lowerClosure (⇑f '' s)) ↔ x✝ ∈ ↑((LowerSet.map f.symm).symm (lowerClosure s))

Tactic:
simp [-LowerSet.symm_map, LowerSet.map, OrderIso.symm, ← f.symm_apply_le]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_neg_right (x y : E) : ⟪x, -y⟫ = -⟪x, y⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ (starRingEnd 𝕜) (-⟪y, x⟫_𝕜) = -⟪x, y⟫_𝕜

Tactic:
simp only [RingHom.map_neg, inner_conj_symm]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ ⟪x, -y⟫_𝕜 = -⟪x, y⟫_𝕜

Tactic:
rw [← inner_conj_symm, inner_neg_left]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ (starRingEnd 𝕜) (-⟪y, x⟫_𝕜) = -⟪x, y⟫_𝕜