harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem add_sub_add_right (n k m : Nat) : (n + k) - (m + k) = n - m

Proof state:
n k m : Nat
⊢ n + k - (m + k) = n - m

Tactic:
induction k with
| zero => simp
| succ k ih => simp [← Nat.add_assoc, succ_sub_succ_eq_sub, ih]

Result:
no goals

Proof state:
case succ
n m k : Nat
ih : n + k - (m + k) = n - m
⊢ n + (k + 1) - (m + (k + 1)) = n - m

Tactic:
simp [← Nat.add_assoc, succ_sub_succ_eq_sub, ih]

Result:
no goals

Proof state:
case zero
n m : Nat
⊢ n + 0 - (m + 0) = n - m

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma pOpcycles_opcyclesIsoSc'_hom :
    K.pOpcycles j ≫ (K.opcyclesIsoSc' i j k hi hk).hom = (K.sc' i j k).pOpcycles

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ ((natIsoSc' C c i j k hi hk).hom.app K).τ₂ ≫ (K.sc' i j k).pOpcycles = (K.sc' i j k).pOpcycles

Tactic:
apply id_comp

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ K.pOpcycles j ≫ (K.opcyclesIsoSc' i j k hi hk).hom = (K.sc' i j k).pOpcycles

Tactic:
dsimp [opcyclesIsoSc']

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ K.pOpcycles j ≫ ShortComplex.opcyclesMap ((natIsoSc' C c i j k hi hk).hom.app K) = (K.sc' i j k).pOpcycles

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ K.pOpcycles j ≫ ShortComplex.opcyclesMap ((natIsoSc' C c i j k hi hk).hom.app K) = (K.sc' i j k).pOpcycles

Tactic:
erw [ShortComplex.p_opcyclesMap]

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ ((natIsoSc' C c i j k hi hk).hom.app K).τ₂ ≫ (K.sc' i j k).pOpcycles = (K.sc' i j k).pOpcycles
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma preimage_coe_Ioc (x y : ℝ) : Real.toEReal ⁻¹' Ioc x y = Ioc x y

Proof state:
x y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ↑x ∩ Iic ↑y) = Ioi x ∩ Iic y

Tactic:
simp

Result:
no goals

Proof state:
x y : ℝ
⊢ Real.toEReal ⁻¹' Ioc ↑x ↑y = Ioc x y

Tactic:
simp_rw [← Ioi_inter_Iic]

Result:
x y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ↑x ∩ Iic ↑y) = Ioi x ∩ Iic y
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
lemma atTop_basis_Ioi' [NoMaxOrder α] (a : α) : atTop.HasBasis (a < ·) Ioi

Proof state:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : NoMaxOrder α
a : α
this : Nonempty α
b : α
x✝ : True
⊢ ∃ i', a < i' ∧ Ioi i' ⊆ Ioi b

Tactic:
obtain ⟨c, hac, hbc⟩ := exists_ge_ge a b

Result:
case intro.intro
α : Type u_3
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : NoMaxOrder α
a : α
this : Nonempty α
b : α
x✝ : True
c : α
hac : a ≤ c
hbc : b ≤ c
⊢ ∃ i', a < i' ∧ Ioi i' ⊆ Ioi b

Proof state:
case intro.intro.intro
α : Type u_3
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : NoMaxOrder α
a : α
this : Nonempty α
b : α
x✝ : True
c : α
hac : a ≤ c
hbc : b ≤ c
d : α
hcd : c < d
⊢ ∃ i', a < i' ∧ Ioi i' ⊆ Ioi b

Tactic:
exact ⟨d, hac.trans_lt hcd, Ioi_subset_Ioi (hbc.trans hcd.le)⟩

Result:
no goals

Proof state:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : NoMaxOrder α
a : α
⊢ atTop.HasBasis (fun x => a < x) Ioi

Tactic:
have : Nonempty α := ⟨a⟩

Result:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : NoMaxOrder α
a : α
this : Nonempty α
⊢ atTop.HasBasis (fun x => a < x) Ioi

Proof state:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : NoMaxOrder α
a : α
this : Nonempty α
⊢ atTop.HasBasis (fun x => a < x) Ioi

Tactic:
refine atTop_basis_Ioi.to_hasBasis (fun b _ ↦ ?_) fun b _ ↦ ⟨b, trivial, Subset.rfl⟩

Result:
α : Type u_3
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : NoMaxOrder α
a : α
this : Nonempty α
b : α
x✝ : True
⊢ ∃ i', a < i' ∧ Ioi i' ⊆ Ioi b

Proof state:
case intro.intro
α : Type u_3
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : NoMaxOrder α
a : α
this : Nonempty α
b : α
x✝ : True
c : α
hac : a ≤ c
hbc : b ≤ c
⊢ ∃ i', a < i' ∧ Ioi i' ⊆ Ioi b

Tactic:
obtain ⟨d, hcd⟩ := exists_gt c

Result:
case intro.intro.intro
α : Type u_3
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
inst✝ : NoMaxOrder α
a : α
this : Nonempty α
b : α
x✝ : True
c : α
hac : a ≤ c
hbc : b ≤ c
d : α
hcd : c < d
⊢ ∃ i', a < i' ∧ Ioi i' ⊆ Ioi b
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
/-- The norm, relative to `ℤ`, of `ζ - 1` in a `p`-th cyclotomic extension of `ℚ` is `p` if
`p ≠ 2`. -/
lemma norm_toInteger_sub_one_of_prime_ne_two' [hcycl : IsCyclotomicExtension {p} ℚ K]
    (hζ : IsPrimitiveRoot ζ p) (h : p ≠ 2) : Algebra.norm ℤ (hζ.toInteger - 1) = p

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
h : p ≠ 2
⊢ IsCyclotomicExtension {p ^ (0 + 1)} ℚ K

Tactic:
simpa using hcycl

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
h : p ≠ 2
⊢ (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p

Tactic:
have : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K := by simpa using hcycl

Result:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
h : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
h : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ (Algebra.norm ℤ) (hζ.toInteger - 1) = ↑↑p

Tactic:
replace hζ : IsPrimitiveRoot ζ (p ^ (0 + 1)) := by simpa using hζ

Result:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ✝ : IsPrimitiveRoot ζ ↑p
h : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))
⊢ (Algebra.norm ℤ) (hζ✝.toInteger - 1) = ↑↑p

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
h : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
⊢ IsPrimitiveRoot ζ (↑p ^ (0 + 1))

Tactic:
simpa using hζ

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p} ℚ K
hζ✝ : IsPrimitiveRoot ζ ↑p
h : p ≠ 2
this : IsCyclotomicExtension {p ^ (0 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (↑p ^ (0 + 1))
⊢ (Algebra.norm ℤ) (hζ✝.toInteger - 1) = ↑↑p

Tactic:
exact hζ.norm_toInteger_sub_one_of_prime_ne_two h

Result:
no goals
-- Mathlib/Data/Real/Archimedean.lean
/-- As `sSup s = 0` when `s` is an empty set of reals, it suffices to show that all elements of `s`
are at most some nonnegative number `a` to show that `sSup s ≤ a`.

See also `csSup_le`. -/
protected lemma sSup_le (hs : ∀ x ∈ s, x ≤ a) (ha : 0 ≤ a) : sSup s ≤ a

Proof state:
s : Set ℝ
a : ℝ
hs : ∀ x ∈ s, x ≤ a
ha : 0 ≤ a
⊢ sSup s ≤ a

Tactic:
obtain rfl | hs' := s.eq_empty_or_nonempty

Result:
case inl
a : ℝ
ha : 0 ≤ a
hs : ∀ x ∈ ∅, x ≤ a
⊢ sSup ∅ ≤ a

case inr
s : Set ℝ
a : ℝ
hs : ∀ x ∈ s, x ≤ a
ha : 0 ≤ a
hs' : s.Nonempty
⊢ sSup s ≤ a

Proof state:
case inl
a : ℝ
ha : 0 ≤ a
hs : ∀ x ∈ ∅, x ≤ a
⊢ sSup ∅ ≤ a

case inr
s : Set ℝ
a : ℝ
hs : ∀ x ∈ s, x ≤ a
ha : 0 ≤ a
hs' : s.Nonempty
⊢ sSup s ≤ a

Tactic:
exacts [sSup_empty.trans_le ha, csSup_le hs' hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem DistinctKeys.alterKey {a : α} {f : Option (β a) → Option (β a)}
    {l : List ((a : α) × β a)} (hl : DistinctKeys l) : DistinctKeys (alterKey a f l)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ DistinctKeys (List.alterKey a f l)

Tactic:
dsimp only [List.alterKey]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ DistinctKeys
    (match f (getValueCast? a l) with
    | none => List.eraseKey a l
    | some v => List.insertEntry a v l)

Proof state:
case h_1
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l : List ((a : α) × β a)
hl : DistinctKeys l
x✝ : Option (β a)
heq✝ : f (getValueCast? a l) = none
⊢ DistinctKeys (List.eraseKey a l)

Tactic:
exact DistinctKeys.eraseKey hl

Result:
no goals

Proof state:
case h_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l : List ((a : α) × β a)
hl : DistinctKeys l
x✝ : Option (β a)
v✝ : β a
heq✝ : f (getValueCast? a l) = some v✝
⊢ DistinctKeys (List.insertEntry a v✝ l)

Tactic:
exact DistinctKeys.insertEntry hl

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l : List ((a : α) × β a)
hl : DistinctKeys l
⊢ DistinctKeys
    (match f (getValueCast? a l) with
    | none => List.eraseKey a l
    | some v => List.insertEntry a v l)

Tactic:
split

Result:
case h_1
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l : List ((a : α) × β a)
hl : DistinctKeys l
x✝ : Option (β a)
heq✝ : f (getValueCast? a l) = none
⊢ DistinctKeys (List.eraseKey a l)

case h_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
f : Option (β a) → Option (β a)
l : List ((a : α) × β a)
hl : DistinctKeys l
x✝ : Option (β a)
v✝ : β a
heq✝ : f (getValueCast? a l) = some v✝
⊢ DistinctKeys (List.insertEntry a v✝ l)
-- Mathlib/Data/List/SplitLengths.lean
theorem length_mem_splitLengths {α : Type*} (l : List α) (sz : List ℕ) (b : ℕ)
    (h : ∀ n ∈ sz, n ≤ b) : ∀ l₂ ∈ sz.splitLengths l, l₂.length ≤ b

Proof state:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ (sz.splitLengths l)[i].length ≤ b

Tactic:
have := length_splitLengths_getElem_le l sz (hi := hi)

Result:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
i : ℕ
hi : i < (sz.splitLengths l).length
this : (sz.splitLengths l)[i].length ≤ sz[i]
⊢ (sz.splitLengths l)[i].length ≤ b

Proof state:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
⊢ ∀ (i : ℕ) (h : i < (sz.splitLengths l).length), (sz.splitLengths l)[i].length ≤ b

Tactic:
intro i hi

Result:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
i : ℕ
hi : i < (sz.splitLengths l).length
⊢ (sz.splitLengths l)[i].length ≤ b

Proof state:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
i : ℕ
hi : i < (sz.splitLengths l).length
this : (sz.splitLengths l)[i].length ≤ sz[i]
⊢ i < sz.length

Tactic:
simpa using hi

Result:
no goals

Proof state:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
i : ℕ
hi : i < (sz.splitLengths l).length
this : (sz.splitLengths l)[i].length ≤ sz[i]
⊢ (sz.splitLengths l)[i].length ≤ b

Tactic:
have := h (sz[i]'(by simpa using hi)) (getElem_mem ..)

Result:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
i : ℕ
hi : i < (sz.splitLengths l).length
this✝ : (sz.splitLengths l)[i].length ≤ sz[i]
this : sz[i] ≤ b
⊢ (sz.splitLengths l)[i].length ≤ b

Proof state:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
⊢ ∀ (l₂ : List α), l₂ ∈ sz.splitLengths l → l₂.length ≤ b

Tactic:
rw [← List.forall_getElem]

Result:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
⊢ ∀ (i : ℕ) (h : i < (sz.splitLengths l).length), (sz.splitLengths l)[i].length ≤ b

Proof state:
α : Type u_2
l : List α
sz : List ℕ
b : ℕ
h : ∀ (n : ℕ), n ∈ sz → n ≤ b
i : ℕ
hi : i < (sz.splitLengths l).length
this✝ : (sz.splitLengths l)[i].length ≤ sz[i]
this : sz[i] ≤ b
⊢ (sz.splitLengths l)[i].length ≤ b

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem dvd_derivative_iff {P : R[X]} : P ∣ derivative P ↔ derivative P = 0 where
  mp h

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
h : derivative P = 0
⊢ P ∣ derivative P

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
h : P ∣ derivative P
⊢ derivative P = 0

Tactic:
by_cases hP : P = 0

Result:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
h : P ∣ derivative P
hP : P = 0
⊢ derivative P = 0

case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
h : P ∣ derivative P
hP : ¬P = 0
⊢ derivative P = 0

Proof state:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
h : P ∣ derivative P
hP : P = 0
⊢ derivative P = 0

Tactic:
simp only [hP, derivative_zero]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
P : R[X]
h : P ∣ derivative P
hP : ¬P = 0
⊢ derivative P = 0

Tactic:
exact eq_zero_of_dvd_of_degree_lt h (degree_derivative_lt hP)

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

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

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

Result:
no goals

Proof state:
case h.e'_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i = if i ∈ s then g i else 0

Tactic:
exact (if_pos hi).symm

Result:
no goals

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

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

Result:
no goals

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

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

Result:
no goals

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

Tactic:
convert
  H s (fun j => if j ∈ s then g j else 0) (fun j hj => if_neg hj)
    (by simp_rw [ite_smul, zero_smul, Finset.sum_extend_by_zero, hg]) i

Result:
case h.e'_2
ι : Type u'
R : Type u_2
M : Type u_4
v : ι → M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
H : ∀ (s : Finset ι) (g : ι → R), (∀ i ∉ s, g i = 0) → ∑ i ∈ s, g i • v i = 0 → ∀ (i : ι), g i = 0
s : Finset ι
g : ι → R
hg : ∑ i ∈ s, g i • v i = 0
i : ι
hi : i ∈ s
⊢ g i = if i ∈ s then g i else 0
-- Mathlib/Data/Multiset/UnionInter.lean
lemma add_eq_union_left_of_le [DecidableEq α] {s t u : Multiset α} (h : t ≤ s) :
    u + s = u ∪ t ↔ Disjoint u s ∧ s = t

Proof state:
case refine_2.intro
α : Type u_1
inst✝ : DecidableEq α
s u : Multiset α
h0 : u + s = u ∪ s
h : s ≤ s
⊢ u + s = u ∪ s

Tactic:
exact h0

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
⊢ u + s = u ∪ t ↔ _root_.Disjoint u s ∧ s = t

Tactic:
rw [← add_eq_union_iff_disjoint]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
⊢ u + s = u ∪ t ↔ u + s = u ∪ s ∧ s = t

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ s = t → u + s = u ∪ s

Tactic:
rintro rfl

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s u : Multiset α
h : s ≤ s
h0 : u + s = u ∪ s
⊢ u + s = u ∪ s

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ u + s = u ∪ s ∧ s = t

Tactic:
rw [and_iff_right_of_imp]

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ s = t

case refine_1
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ s = t → u + s = u ∪ s

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ s = t

Tactic:
exact (Multiset.le_of_add_le_add_left <| h0.trans_le <| union_le_add u t).antisymm h

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
⊢ u + s = u ∪ s ∧ s = t → u + s = u ∪ t

Tactic:
rintro ⟨h0, rfl⟩

Result:
case refine_2.intro
α : Type u_1
inst✝ : DecidableEq α
s u : Multiset α
h0 : u + s = u ∪ s
h : s ≤ s
⊢ u + s = u ∪ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
⊢ u + s = u ∪ t ↔ u + s = u ∪ s ∧ s = t

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

Result:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
h0 : u + s = u ∪ t
⊢ u + s = u ∪ s ∧ s = t

case refine_2
α : Type u_1
inst✝ : DecidableEq α
s t u : Multiset α
h : t ≤ s
⊢ u + s = u ∪ s ∧ s = t → u + s = u ∪ t

Proof state:
case refine_1
α : Type u_1
inst✝ : DecidableEq α
s u : Multiset α
h : s ≤ s
h0 : u + s = u ∪ s
⊢ u + s = u ∪ s

Tactic:
exact h0

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/TruncGEHomology.lean
lemma hasHomology_sc'_of_not_mem_boundary (hj : ¬ e.BoundaryGE j) :
    ((K.truncGE' e).sc' i j k).HasHomology

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this✝ : (K.restriction e).HasHomology j
this : ((K.restriction e).sc' i j k).HasHomology
φ : (shortComplexFunctor' C c i j k).obj (K.restriction e) ⟶ (shortComplexFunctor' C c i j k).obj (K.truncGE' e) :=
  (shortComplexFunctor' C c i j k).map (K.restrictionToTruncGE' e)
⊢ Epi φ.τ₁

Tactic:
dsimp [φ]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this✝ : (K.restriction e).HasHomology j
this : ((K.restriction e).sc' i j k).HasHomology
φ : (shortComplexFunctor' C c i j k).obj (K.restriction e) ⟶ (shortComplexFunctor' C c i j k).obj (K.truncGE' e) :=
  (shortComplexFunctor' C c i j k).map (K.restrictionToTruncGE' e)
⊢ Epi ((K.restrictionToTruncGE' e).f i)

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this✝¹ : (K.restriction e).HasHomology j
this✝ : ((K.restriction e).sc' i j k).HasHomology
φ : (shortComplexFunctor' C c i j k).obj (K.restriction e) ⟶ (shortComplexFunctor' C c i j k).obj (K.truncGE' e) :=
  (shortComplexFunctor' C c i j k).map (K.restrictionToTruncGE' e)
this : Epi φ.τ₁
⊢ ((K.truncGE' e).sc' i j k).HasHomology

Tactic:
have : IsIso φ.τ₂ := K.isIso_restrictionToTruncGE' e j hj

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this✝² : (K.restriction e).HasHomology j
this✝¹ : ((K.restriction e).sc' i j k).HasHomology
φ : (shortComplexFunctor' C c i j k).obj (K.restriction e) ⟶ (shortComplexFunctor' C c i j k).obj (K.truncGE' e) :=
  (shortComplexFunctor' C c i j k).map (K.restrictionToTruncGE' e)
this✝ : Epi φ.τ₁
this : IsIso φ.τ₂
⊢ ((K.truncGE' e).sc' i j k).HasHomology
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma isDynCoverOf_univ (T : X → X) (F : Set X) (n : ℕ) {s : Set X} (h : s.Nonempty) :
    IsDynCoverOf T F univ n s

Proof state:
X : Type u_1
T : X → X
F : Set X
n : ℕ
s : Set X
h : s.Nonempty
⊢ IsDynCoverOf T F univ n s

Tactic:
simp only [IsDynCoverOf, ball, dynEntourage, Prod.map_iterate, preimage_univ, iInter_univ,
  iUnion_coe_set]

Result:
X : Type u_1
T : X → X
F : Set X
n : ℕ
s : Set X
h : s.Nonempty
⊢ F ⊆ ⋃ x ∈ s, univ

Proof state:
case intro
X : Type u_1
T : X → X
F : Set X
n : ℕ
s : Set X
x : X
x_s : x ∈ s
⊢ F ⊆ ⋃ x ∈ s, univ

Tactic:
exact subset_iUnion₂_of_subset x x_s (subset_univ F)

Result:
no goals

Proof state:
X : Type u_1
T : X → X
F : Set X
n : ℕ
s : Set X
h : s.Nonempty
⊢ F ⊆ ⋃ x ∈ s, univ

Tactic:
rcases h with ⟨x, x_s⟩

Result:
case intro
X : Type u_1
T : X → X
F : Set X
n : ℕ
s : Set X
x : X
x_s : x ∈ s
⊢ F ⊆ ⋃ x ∈ s, univ
-- Mathlib/CategoryTheory/Sites/Sieves.lean
@[simp]
lemma comp_mem_iff (i : X ⟶ Y) (f : Y ⟶ Z) [IsIso i] (S : Sieve Z) :
    S (i ≫ f) ↔ S f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
i : X ⟶ Y
f : Y ⟶ Z
inst✝ : IsIso i
S : Sieve Z
H : S.arrows (i ≫ f)
⊢ S.arrows f

Tactic:
convert S.downward_closed H (inv i)

Result:
case h.e'_6
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
i : X ⟶ Y
f : Y ⟶ Z
inst✝ : IsIso i
S : Sieve Z
H : S.arrows (i ≫ f)
⊢ f = inv i ≫ i ≫ f

Proof state:
case h.e'_6
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
i : X ⟶ Y
f : Y ⟶ Z
inst✝ : IsIso i
S : Sieve Z
H : S.arrows (i ≫ f)
⊢ f = inv i ≫ i ≫ f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
i : X ⟶ Y
f : Y ⟶ Z
inst✝ : IsIso i
S : Sieve Z
⊢ S.arrows (i ≫ f) ↔ S.arrows f

Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ S.downward_closed H _⟩

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
i : X ⟶ Y
f : Y ⟶ Z
inst✝ : IsIso i
S : Sieve Z
H : S.arrows (i ≫ f)
⊢ S.arrows f