harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem _root_.IsFractional.inf_right {I : Submodule R P} :
    IsFractional S I → ∀ J, IsFractional S (I ⊓ J)
  | ⟨aI, haI, hI⟩, J =>
    ⟨aI, haI, fun b hb => by
      rcases mem_inf.mp hb with ⟨hbI, _⟩
      exact hI b hbI⟩

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
J : Submodule R P
b : P
hb : b ∈ I ⊓ J
⊢ IsInteger R (aI • b)

Tactic:
rcases mem_inf.mp hb with ⟨hbI, _⟩

Result:
case intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
J : Submodule R P
b : P
hb : b ∈ I ⊓ J
hbI : b ∈ I
right✝ : b ∈ J
⊢ IsInteger R (aI • b)

Proof state:
case intro
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I : Submodule R P
aI : R
haI : aI ∈ S
hI : ∀ b ∈ I, IsInteger R (aI • b)
J : Submodule R P
b : P
hb : b ∈ I ⊓ J
hbI : b ∈ I
right✝ : b ∈ J
⊢ IsInteger R (aI • b)

Tactic:
exact hI b hbI

Result:
no goals
-- Mathlib/RingTheory/Polynomial/UniqueFactorization.lean
theorem exists_irreducible_of_natDegree_pos (hf : 0 < f.natDegree) : ∃ g, Irreducible g ∧ g ∣ f :=
  exists_irreducible_of_degree_pos <| by
    contrapose! hf
    exact natDegree_le_of_degree_le hf

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
f : R[X]
hf : 0 < f.natDegree
⊢ 0 < f.degree

Tactic:
contrapose! hf

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
f : R[X]
hf : f.degree ≤ 0
⊢ f.natDegree ≤ 0

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : WfDvdMonoid R
f : R[X]
hf : f.degree ≤ 0
⊢ f.natDegree ≤ 0

Tactic:
exact natDegree_le_of_degree_le hf

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem zpow_apply_eq_self_of_apply_eq_self {x : α} (hfx : f x = x) : ∀ n : ℤ, (f ^ n) x = x
  | (n : ℕ) => pow_apply_eq_self_of_apply_eq_self hfx n
  | Int.negSucc n => by rw [zpow_negSucc, inv_eq_iff_eq, pow_apply_eq_self_of_apply_eq_self hfx]

Proof state:
α : Type u_1
f : Perm α
x : α
hfx : f x = x
n : ℕ
⊢ (f ^ Int.negSucc n) x = x

Tactic:
rw [zpow_negSucc, inv_eq_iff_eq, pow_apply_eq_self_of_apply_eq_self hfx]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem lt_length_iff' {s : Seq α} {n : ℕ} :
    (∀ h : s.Terminates, n < s.length h) ↔ ∃ a, a ∈ s.get? n

Proof state:
α : Type u
s : Seq α
n : ℕ
⊢ (∀ (h : s.Terminates), n < s.length h) ↔ ∃ a, a ∈ s.get? n

Tactic:
simp only [Terminates, TerminatedAt, length, Nat.lt_find_iff, forall_exists_index, Option.mem_def,
  ← Option.ne_none_iff_exists', ne_eq]

Result:
α : Type u
s : Seq α
n : ℕ
⊢ (∀ (x : ℕ), s.get? x = none → ∀ (m : ℕ), m ≤ n → ¬s.get? m = none) ↔ ¬s.get? n = none

Proof state:
case refine_1
α : Type u
s : Seq α
n : ℕ
⊢ (∀ (x : ℕ), s.get? x = none → ∀ (m : ℕ), m ≤ n → ¬s.get? m = none) → ¬s.get? n = none

Tactic:
intro h hn

Result:
case refine_1
α : Type u
s : Seq α
n : ℕ
h : ∀ (x : ℕ), s.get? x = none → ∀ (m : ℕ), m ≤ n → ¬s.get? m = none
hn : s.get? n = none
⊢ False

Proof state:
case refine_1
α : Type u
s : Seq α
n : ℕ
h : ∀ (x : ℕ), s.get? x = none → ∀ (m : ℕ), m ≤ n → ¬s.get? m = none
hn : s.get? n = none
⊢ False

Tactic:
exact h n hn n le_rfl hn

Result:
no goals

Proof state:
α : Type u
s : Seq α
n : ℕ
⊢ (∀ (x : ℕ), s.get? x = none → ∀ (m : ℕ), m ≤ n → ¬s.get? m = none) ↔ ¬s.get? n = none

Tactic:
refine ⟨?_, ?_⟩

Result:
case refine_1
α : Type u
s : Seq α
n : ℕ
⊢ (∀ (x : ℕ), s.get? x = none → ∀ (m : ℕ), m ≤ n → ¬s.get? m = none) → ¬s.get? n = none

case refine_2
α : Type u
s : Seq α
n : ℕ
⊢ ¬s.get? n = none → ∀ (x : ℕ), s.get? x = none → ∀ (m : ℕ), m ≤ n → ¬s.get? m = none

Proof state:
case refine_2
α : Type u
s : Seq α
n : ℕ
⊢ ¬s.get? n = none → ∀ (x : ℕ), s.get? x = none → ∀ (m : ℕ), m ≤ n → ¬s.get? m = none

Tactic:
intro hn _ _ k hkn hk

Result:
case refine_2
α : Type u
s : Seq α
n : ℕ
hn : ¬s.get? n = none
x✝ : ℕ
h✝ : s.get? x✝ = none
k : ℕ
hkn : k ≤ n
hk : s.get? k = none
⊢ False

Proof state:
case refine_2
α : Type u
s : Seq α
n : ℕ
hn : ¬s.get? n = none
x✝ : ℕ
h✝ : s.get? x✝ = none
k : ℕ
hkn : k ≤ n
hk : s.get? k = none
⊢ False

Tactic:
exact hn <| le_stable s hkn hk

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
/-- A module generated by semisimple submodules is itself semisimple. -/
lemma isSemisimpleModule_of_isSemisimpleModule_submodule {s : Set ι} {p : ι → Submodule R M}
    (hp : ∀ i ∈ s, IsSemisimpleModule R (p i)) (hp' : ⨆ i ∈ s, p i = ⊤) :
    IsSemisimpleModule R M

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
hp' : ⨆ i ∈ s, p i = ⊤
⊢ IsSemisimpleModule R M

Tactic:
refine complementedLattice_of_complementedLattice_Iic (fun i hi ↦ ?_) hp'

Result:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
hp' : ⨆ i ∈ s, p i = ⊤
i : ι
hi : i ∈ s
⊢ ComplementedLattice ↑(Set.Iic (p i))

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
hp' : ⨆ i ∈ s, p i = ⊤
i : ι
hi : i ∈ s
⊢ ComplementedLattice ↑(Set.Iic (p i))

Tactic:
simpa only [← (p i).mapIic.complementedLattice_iff] using hp i hi

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
/-- The iterated derivative commutes with shifting the function by a constant on the right. -/
lemma iteratedFDeriv_comp_add_right' (n : ℕ) (a : E) :
    iteratedFDeriv 𝕜 n (fun z ↦ f (z + a)) = fun x ↦ iteratedFDeriv 𝕜 n f (x + a)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : ℕ
a : E
⊢ (iteratedFDeriv 𝕜 n fun z => f (z + a)) = fun x => iteratedFDeriv 𝕜 n f (x + a)

Tactic:
simpa [add_comm a] using iteratedFDeriv_comp_add_left' n a

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean
theorem spineToSimplex_interval (f : Path X n) (j l : ℕ) (hjl : j + l ≤  n)  :
    X.map (subinterval j l hjl).op (spineToSimplex f) =
      spineToSimplex (Path.interval f j l hjl)

Proof state:
case a
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ X.spine l (X.map (subinterval j l hjl).op (spineToSimplex f)) = f.interval j l hjl

Tactic:
convert spine_map_subinterval X j l hjl (spineToSimplex f)

Result:
case h.e'_3.h.e'_3
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ f = X.spine n (spineToSimplex f)

Proof state:
case a
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ { toFun := X.spine l, invFun := spineToSimplex, left_inv := ⋯, right_inv := ⋯ }
      (X.map (subinterval j l hjl).op (spineToSimplex f)) =
    { toFun := X.spine l, invFun := spineToSimplex, left_inv := ⋯, right_inv := ⋯ }
      (spineToSimplex (f.interval j l hjl))

Tactic:
dsimp

Result:
case a
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ X.spine l (X.map (subinterval j l hjl).op (spineToSimplex f)) = X.spine l (spineToSimplex (f.interval j l hjl))

Proof state:
case h.e'_3.h.e'_3
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ f = X.spine n (spineToSimplex f)

Tactic:
exact Eq.symm (spine_spineToSimplex f)

Result:
no goals

Proof state:
case a
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ X.spine l (X.map (subinterval j l hjl).op (spineToSimplex f)) = X.spine l (spineToSimplex (f.interval j l hjl))

Tactic:
rw [spine_spineToSimplex]

Result:
case a
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ X.spine l (X.map (subinterval j l hjl).op (spineToSimplex f)) = f.interval j l hjl

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ X.map (subinterval j l hjl).op (spineToSimplex f) = spineToSimplex (f.interval j l hjl)

Tactic:
apply spineInjective

Result:
case a
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ (spineEquiv l) (X.map (subinterval j l hjl).op (spineToSimplex f)) =
    (spineEquiv l) (spineToSimplex (f.interval j l hjl))

Proof state:
case a
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ (spineEquiv l) (X.map (subinterval j l hjl).op (spineToSimplex f)) =
    (spineEquiv l) (spineToSimplex (f.interval j l hjl))

Tactic:
unfold spineEquiv

Result:
case a
X : SSet
inst✝ : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ { toFun := X.spine l, invFun := spineToSimplex, left_inv := ⋯, right_inv := ⋯ }
      (X.map (subinterval j l hjl).op (spineToSimplex f)) =
    { toFun := X.spine l, invFun := spineToSimplex, left_inv := ⋯, right_inv := ⋯ }
      (spineToSimplex (f.interval j l hjl))
-- Mathlib/ModelTheory/Definability.lean
theorem Definable.compl {s : Set (α → M)} (hf : A.Definable L s) : A.Definable L sᶜ

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
hf : A.Definable L s
⊢ A.Definable L sᶜ

Tactic:
rcases hf with ⟨φ, hφ⟩

Result:
case intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L[[↑A]].Formula α
hφ : s = setOf φ.Realize
⊢ A.Definable L sᶜ

Proof state:
case intro.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L[[↑A]].Formula α
hφ : s = setOf φ.Realize
v : α → M
⊢ v ∈ sᶜ ↔ v ∈ setOf φ.not.Realize

Tactic:
rw [hφ, compl_setOf, mem_setOf, mem_setOf, Formula.realize_not]

Result:
no goals

Proof state:
case intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L[[↑A]].Formula α
hφ : s = setOf φ.Realize
⊢ A.Definable L sᶜ

Tactic:
refine ⟨φ.not, ?_⟩

Result:
case intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L[[↑A]].Formula α
hφ : s = setOf φ.Realize
⊢ sᶜ = setOf φ.not.Realize

Proof state:
case intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L[[↑A]].Formula α
hφ : s = setOf φ.Realize
⊢ sᶜ = setOf φ.not.Realize

Tactic:
ext v

Result:
case intro.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
s : Set (α → M)
φ : L[[↑A]].Formula α
hφ : s = setOf φ.Realize
v : α → M
⊢ v ∈ sᶜ ↔ v ∈ setOf φ.not.Realize
-- Mathlib/GroupTheory/Coxeter/Length.lean
theorem not_isRightDescent_iff {w : W} {i : B} :
    ¬cs.IsRightDescent w i ↔ ℓ (w * s i) = ℓ w + 1

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ ¬cs.length (w * cs.simple i) < cs.length w ↔ cs.length (w * cs.simple i) = cs.length w + 1

Tactic:
constructor

Result:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ ¬cs.length (w * cs.simple i) < cs.length w → cs.length (w * cs.simple i) = cs.length w + 1

case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) = cs.length w + 1 → ¬cs.length (w * cs.simple i) < cs.length w

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
a✝ : ¬cs.length (w * cs.simple i) < cs.length w
⊢ ¬cs.length (w * cs.simple i) + 1 = cs.length w

Tactic:
omega

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ ¬cs.IsRightDescent w i ↔ cs.length (w * cs.simple i) = cs.length w + 1

Tactic:
unfold IsRightDescent

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ ¬cs.length (w * cs.simple i) < cs.length w ↔ cs.length (w * cs.simple i) = cs.length w + 1

Proof state:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ ¬cs.length (w * cs.simple i) < cs.length w → cs.length (w * cs.simple i) = cs.length w + 1

Tactic:
intro _

Result:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
a✝ : ¬cs.length (w * cs.simple i) < cs.length w
⊢ cs.length (w * cs.simple i) = cs.length w + 1

Proof state:
case mpr
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
⊢ cs.length (w * cs.simple i) = cs.length w + 1 → ¬cs.length (w * cs.simple i) < cs.length w

Tactic:
omega

Result:
no goals

Proof state:
case mp
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
w : W
i : B
a✝ : ¬cs.length (w * cs.simple i) < cs.length w
⊢ cs.length (w * cs.simple i) = cs.length w + 1

Tactic:
exact (cs.length_mul_simple w i).resolve_right (by omega)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem ae_restrict_biUnion_eq (s : ι → Set α) {t : Set ι} (ht : t.Countable) :
    ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i))

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
⊢ ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i))

Tactic:
haveI := ht.to_subtype

Result:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
this : Countable ↑t
⊢ ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i))

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
s : ι → Set α
t : Set ι
ht : t.Countable
this : Countable ↑t
⊢ ae (μ.restrict (⋃ i ∈ t, s i)) = ⨆ i ∈ t, ae (μ.restrict (s i))

Tactic:
rw [biUnion_eq_iUnion, ae_restrict_iUnion_eq, ← iSup_subtype'']

Result:
no goals
-- Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
theorem linearIndependent_iff''ₛ :
    LinearIndependent R v ↔
      ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) →
        ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ i, f i = g i

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ ∑ i ∈ s, (fun j => if j ∈ s then f j else 0) i • v i = ∑ i ∈ s, (fun j => if j ∈ s then g j else 0) i • v i

Tactic:
simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
H :
  ∀ (s : Finset ι) (f g : ι → R), (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i
s : Finset ι
f g : ι → R
eq : ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i
i : ι
hi : i ∈ s
⊢ f i = g i

Tactic:
convert
  H s (fun j ↦ if j ∈ s then f j else 0) (fun j ↦ if j ∈ s then g j else 0)
    (fun j hj ↦ (if_neg hj).trans (if_neg hj).symm)
    (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]) i <;>
exact (if_pos hi).symm

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ LinearIndependent R v ↔
    ∀ (s : Finset ι) (f g : ι → R),
      (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i

Tactic:
classical
exact linearIndependent_iff'ₛ.trans
  ⟨fun H s f g eq hv i ↦ if his : i ∈ s then H s f g hv i his else eq i his,
    fun H s f g eq i hi ↦ by
    convert
      H s (fun j ↦ if j ∈ s then f j else 0) (fun j ↦ if j ∈ s then g j else 0)
        (fun j hj ↦ (if_neg hj).trans (if_neg hj).symm)
        (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]) i <;>
    exact (if_pos hi).symm⟩

Result:
no goals

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ LinearIndependent R v ↔
    ∀ (s : Finset ι) (f g : ι → R),
      (∀ i ∉ s, f i = g i) → ∑ i ∈ s, f i • v i = ∑ i ∈ s, g i • v i → ∀ (i : ι), f i = g i

Tactic:
exact linearIndependent_iff'ₛ.trans
  ⟨fun H s f g eq hv i ↦ if his : i ∈ s then H s f g hv i his else eq i his,
    fun H s f g eq i hi ↦ by
    convert
      H s (fun j ↦ if j ∈ s then f j else 0) (fun j ↦ if j ∈ s then g j else 0)
        (fun j hj ↦ (if_neg hj).trans (if_neg hj).symm)
        (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, eq]) i <;>
    exact (if_pos hi).symm⟩

Result:
no goals
-- Mathlib/Logic/Hydra.lean
/-- `CutExpand` preserves leftward-closedness under a relation. -/
lemma cutExpand_closed [IsIrrefl α r] (p : α → Prop)
    (h : ∀ {a' a}, r a' a → p a → p a') {s' s : Multiset α} :
    CutExpand r s' s → (∀ a ∈ s, p a) → ∀ a ∈ s', p a

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s' s : Multiset α
⊢ CutExpand r s' s → (∀ a ∈ s, p a) → ∀ a ∈ s', p a

Tactic:
rw [cutExpand_iff]

Result:
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s' s : Multiset α
⊢ (∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t) → (∀ a ∈ s, p a) → ∀ a ∈ s', p a

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s' s : Multiset α
⊢ (∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t) → (∀ a ∈ s, p a) → ∀ a ∈ s', p a

Tactic:
rintro ⟨t, a, hr, ha, rfl⟩ hsp a' h'

Result:
case intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
ha : a ∈ s
hsp : ∀ a ∈ s, p a
a' : α
h' : a' ∈ s.erase a + t
⊢ p a'

Proof state:
case intro.intro.intro.intro.inl
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
ha : a ∈ s
hsp : ∀ a ∈ s, p a
a' : α
h'✝ : a' ∈ s.erase a + t
h' : a' ∈ s.erase a
⊢ p a'

case intro.intro.intro.intro.inr
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
ha : a ∈ s
hsp : ∀ a ∈ s, p a
a' : α
h'✝ : a' ∈ s.erase a + t
h' : a' ∈ t
⊢ p a'

Tactic:
exacts [hsp a' (mem_of_mem_erase h'), h (hr a' h') (hsp a ha)]

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
ha : a ∈ s
hsp : ∀ a ∈ s, p a
a' : α
h' : a' ∈ s.erase a + t
⊢ p a'

Tactic:
obtain (h'|h') := mem_add.1 h'

Result:
case intro.intro.intro.intro.inl
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
ha : a ∈ s
hsp : ∀ a ∈ s, p a
a' : α
h'✝ : a' ∈ s.erase a + t
h' : a' ∈ s.erase a
⊢ p a'

case intro.intro.intro.intro.inr
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s t : Multiset α
a : α
hr : ∀ a' ∈ t, r a' a
ha : a ∈ s
hsp : ∀ a ∈ s, p a
a' : α
h'✝ : a' ∈ s.erase a + t
h' : a' ∈ t
⊢ p a'

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsIrrefl α r
p : α → Prop
h : ∀ {a' a : α}, r a' a → p a → p a'
s' s : Multiset α
⊢ CutExpand r s' s → (∀ a ∈ s, p a) → ∀ a ∈ s', p a

Tactic:
classical
rw [cutExpand_iff]
rintro ⟨t, a, hr, ha, rfl⟩ hsp a' h'
obtain (h'|h') := mem_add.1 h'
exacts [hsp a' (mem_of_mem_erase h'), h (hr a' h') (hsp a ha)]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem nextCoeff_map (hf : Injective f) (p : R[X]) : (p.map f).nextCoeff = f p.nextCoeff

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
⊢ (if (map f p).natDegree = 0 then 0 else (map f p).coeff ((map f p).natDegree - 1)) =
    f (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1))

Tactic:
rw [natDegree_map_eq_of_injective hf]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
⊢ (if p.natDegree = 0 then 0 else (map f p).coeff (p.natDegree - 1)) =
    f (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1))

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
⊢ (map f p).nextCoeff = f p.nextCoeff

Tactic:
unfold nextCoeff

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
⊢ (if (map f p).natDegree = 0 then 0 else (map f p).coeff ((map f p).natDegree - 1)) =
    f (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1))

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
hf : Injective ⇑f
p : R[X]
⊢ (if p.natDegree = 0 then 0 else (map f p).coeff (p.natDegree - 1)) =
    f (if p.natDegree = 0 then 0 else p.coeff (p.natDegree - 1))

Tactic:
split_ifs <;> simp [*]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Separated.lean
/--
Suppose `X` is a reduced `S`-scheme and `Y` is a separated `S`-scheme.
For any `S`-morphisms `f g : X ⟶ Y`, `f = g` if `ι ≫ f = ι ≫ g` for some dominant `ι`.
-/
lemma ext_of_isDominant_of_isSeparated' [X.Over S] [Y.Over S] [IsReduced X] [IsSeparated (Y ↘ S)]
    {f g : X ⟶ Y} [f.IsOver S] [g.IsOver S] {W} (ι : W ⟶ X) [IsDominant ι]
    (hU : ι ≫ f = ι ≫ g) : f = g :=
  ext_of_isDominant_of_isSeparated (Y ↘ S) (by simp) ι hU

Proof state:
X Y S : Scheme
inst✝⁶ : X.Over S
inst✝⁵ : Y.Over S
inst✝⁴ : IsReduced X
inst✝³ : IsSeparated (Y ↘ S)
f g : X ⟶ Y
inst✝² : Scheme.Hom.IsOver f S
inst✝¹ : Scheme.Hom.IsOver g S
W : Scheme
ι : W ⟶ X
inst✝ : IsDominant ι
hU : ι ≫ f = ι ≫ g
⊢ f ≫ Y ↘ S = g ≫ Y ↘ S

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Triangle.lean
theorem norm_eq_of_angle_sub_eq_angle_sub_rev_of_angle_ne_pi {x y : V}
    (h : angle x (x - y) = angle y (y - x)) (hpi : angle x y ≠ π) : ‖x‖ = ‖y‖

Proof state:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ - ‖y‖ = inner x y * (‖x‖⁻¹ - ‖y‖⁻¹)
hx0 : ¬x = 0
hy0 : y = 0
⊢ ‖x‖ = ‖y‖

Tactic:
rw [hy0, norm_zero, inner_zero_right, zero_mul, sub_zero] at h

Result:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ = 0
hx0 : ¬x = 0
hy0 : y = 0
⊢ ‖x‖ = ‖y‖

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
hx0 : ¬x = 0
hy0 : ¬y = 0
hyx : ¬‖y‖ = ‖x‖
h : inner x y / (‖x‖ * ‖y‖) = -1
⊢ False

Tactic:
rw [real_inner_div_norm_mul_norm_eq_neg_one_iff, ← angle_eq_pi_iff] at h

Result:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
hx0 : ¬x = 0
hy0 : ¬y = 0
hyx : ¬‖y‖ = ‖x‖
h : angle x y = π
⊢ False

Proof state:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖y‖ = 0
hx0 : x = 0
⊢ ‖x‖ = ‖y‖

Tactic:
rw [hx0, norm_zero, h]

Result:
no goals

Proof state:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
hpi : angle x y ≠ π
hxy : ¬x = y
h : ‖x‖ = 0
hx0 : ¬x = 0
hy0 : y = 0
⊢ ‖x‖ = ‖y‖

Tactic:
rw [hy0, norm_zero, h]

Result:
no goals