harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem yn_modEq_two : ∀ n, yn a1 n ≡ n [MOD 2]
  | 0 => by rfl
  | 1 => by simp; rfl
  | n + 2 =>
    (yn_modEq_two n).add_right_cancel <| by
      rw [yn_succ_succ, mul_assoc, (by ring : n + 2 + n = 2 * (n + 1))]
      exact (dvd_mul_right 2 _).modEq_zero_nat.trans (dvd_mul_right 2 _).zero_modEq_nat

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ n + 2 + n = 2 * (n + 1)

Tactic:
ring

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
⊢ yn a1 1 ≡ 1 [MOD 2]

Tactic:
simp

Result:
a : ℕ
a1 : 1 < a
⊢ 1 ≡ 1 [MOD 2]

Proof state:
a : ℕ
a1 : 1 < a
⊢ yn a1 0 ≡ 0 [MOD 2]

Tactic:
rfl

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ yn a1 (n + 2) + yn a1 n ≡ n + 2 + n [MOD 2]

Tactic:
rw [yn_succ_succ, mul_assoc, (by ring : n + 2 + n = 2 * (n + 1))]

Result:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ 2 * (a * yn a1 (n + 1)) ≡ 2 * (n + 1) [MOD 2]

Proof state:
a : ℕ
a1 : 1 < a
n : ℕ
⊢ 2 * (a * yn a1 (n + 1)) ≡ 2 * (n + 1) [MOD 2]

Tactic:
exact (dvd_mul_right 2 _).modEq_zero_nat.trans (dvd_mul_right 2 _).zero_modEq_nat

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
⊢ 1 ≡ 1 [MOD 2]

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_modify (h : m.1.WF) [Inhabited α] {k k' : α} {f : β → β}
    (hc : (Const.modify m k f).contains k') :
    (Const.modify m k f).getKey k' hc =
      if heq : k == k' then
        k
      else
        haveI h' : m.contains k'

Proof state:
α : Type u
β✝ : α → Type v
m✝ : Raw₀ α β✝
inst✝⁵ : BEq α
inst✝⁴ : Hashable α
inst✝³ : LawfulBEq α
β : Type v
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
inst✝ : Inhabited α
k k' : α
f : β → β
hc : (modify m k f).contains k' = true
heq : ¬(k == k') = true
⊢ m.contains k' = true

Tactic:
rwa [contains_modify _ h] at hc

Result:
no goals

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
m : Raw₀ α fun x => β
h : m.val.WF
inst✝ : Inhabited α
k k' : α
f : β → β
hc : (modify m k f).contains k' = true
⊢ (modify m k f).getKey k' hc = if heq : (k == k') = true then k else m.getKey k' ⋯

Tactic:
simp_to_model [Const.modify] using List.Const.getKey_modifyKey

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem factors_right_of_factors_add {X Y : C} {P : Subobject Y} (f g : X ⟶ Y)
    (w : P.Factors (f + g)) (wf : P.Factors f) : P.Factors g :=
  (factors_iff _ _).mpr ⟨P.factorThru (f + g) w - P.factorThru f wf, by simp⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : P.Factors (f + g)
wf : P.Factors f
⊢ (P.factorThru (f + g) w - P.factorThru f wf) ≫ (representative.obj P).arrow = g

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem orthogonalProjection_eq_sum {U : Submodule 𝕜 E} [CompleteSpace U]
    (b : OrthonormalBasis ι 𝕜 U) (x : E) :
    orthogonalProjection U x = ∑ i, ⟪(b i : E), x⟫ • b i

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : RCLike 𝕜
E : Type u_4
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : Fintype ι
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
b : OrthonormalBasis ι 𝕜 ↥U
x : E
⊢ (orthogonalProjection U) x = ∑ i : ι, inner (↑(b i)) x • b i

Tactic:
simpa only [b.repr_apply_apply, inner_orthogonalProjection_eq_of_mem_left] using
  (b.sum_repr (orthogonalProjection U x)).symm

Result:
no goals
-- Mathlib/Data/Nat/Dist.lean
theorem dist_mul_left (k n m : ℕ) : dist (k * n) (k * m) = k * dist n m

Proof state:
k n m : ℕ
⊢ (k * n).dist (k * m) = k * n.dist m

Tactic:
rw [mul_comm k n, mul_comm k m, dist_mul_right, mul_comm]

Result:
no goals
-- Mathlib/Topology/Order.lean
lemma generateFrom_insert_of_generateOpen {α : Type*} {s : Set (Set α)} {t : Set α}
    (ht : GenerateOpen s t) : generateFrom (insert t s) = generateFrom s

Proof state:
α : Type u_1
s : Set (Set α)
t : Set α
ht : GenerateOpen s t
⊢ generateFrom (insert t s) = generateFrom s

Tactic:
refine le_antisymm (generateFrom_anti <| subset_insert t s) (le_generateFrom ?_)

Result:
α : Type u_1
s : Set (Set α)
t : Set α
ht : GenerateOpen s t
⊢ ∀ s_1 ∈ insert t s, IsOpen s_1

Proof state:
α : Type u_1
s : Set (Set α)
t : Set α
ht : GenerateOpen s t
⊢ ∀ s_1 ∈ insert t s, IsOpen s_1

Tactic:
rintro t (rfl | h)

Result:
case inl
α : Type u_1
s : Set (Set α)
t : Set α
ht : GenerateOpen s t
⊢ IsOpen t

case inr
α : Type u_1
s : Set (Set α)
t✝ : Set α
ht : GenerateOpen s t✝
t : Set α
h : t ∈ s
⊢ IsOpen t

Proof state:
case inl
α : Type u_1
s : Set (Set α)
t : Set α
ht : GenerateOpen s t
⊢ IsOpen t

Tactic:
exact ht

Result:
no goals

Proof state:
case inr
α : Type u_1
s : Set (Set α)
t✝ : Set α
ht : GenerateOpen s t✝
t : Set α
h : t ∈ s
⊢ IsOpen t

Tactic:
exact isOpen_generateFrom_of_mem h

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem count_one : count K v (1 : FractionalIdeal R⁰ K) = 0

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
h1 : 1 = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑1
⊢ count K v 1 = 0

Tactic:
rw [count_well_defined K v one_ne_zero h1, Ideal.span_singleton_one, Ideal.one_eq_top, sub_self]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ count K v 1 = 0

Tactic:
have h1 : (1 : FractionalIdeal R⁰ K) =
    spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑(1 : Ideal R) := by
  rw [(algebraMap R K).map_one, Ideal.one_eq_top, coeIdeal_top, mul_one, inv_one,
    spanSingleton_one]

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
h1 : 1 = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑1
⊢ count K v 1 = 0

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
⊢ 1 = spanSingleton R⁰ ((algebraMap R K) 1)⁻¹ * ↑1

Tactic:
rw [(algebraMap R K).map_one, Ideal.one_eq_top, coeIdeal_top, mul_one, inv_one,
  spanSingleton_one]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Basic.lean
theorem coe_vanishingIdeal (t : Set (PrimeSpectrum R)) :
    (vanishingIdeal t : Set R) = { f : R | ∀ x ∈ t, f ∈ x.asIdeal }

Proof state:
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
⊢ ↑(vanishingIdeal t) = {f | ∀ x ∈ t, f ∈ x.asIdeal}

Tactic:
ext f

Result:
case h
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
⊢ f ∈ ↑(vanishingIdeal t) ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asIdeal}

Proof state:
case h
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
⊢ f ∈ ↑(vanishingIdeal t) ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asIdeal}

Tactic:
rw [vanishingIdeal, SetLike.mem_coe, Submodule.mem_iInf]

Result:
case h
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
⊢ (∀ (i : PrimeSpectrum R), f ∈ ⨅ (_ : i ∈ t), i.asIdeal) ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asIdeal}

Proof state:
case h
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
⊢ (∀ (i : PrimeSpectrum R), f ∈ ⨅ (_ : i ∈ t), i.asIdeal) ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asIdeal}

Tactic:
apply forall_congr'

Result:
case h.h
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
⊢ ∀ (a : PrimeSpectrum R), f ∈ ⨅ (_ : a ∈ t), a.asIdeal ↔ a ∈ t → f ∈ a.asIdeal

Proof state:
case h.h
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
⊢ ∀ (a : PrimeSpectrum R), f ∈ ⨅ (_ : a ∈ t), a.asIdeal ↔ a ∈ t → f ∈ a.asIdeal

Tactic:
intro x

Result:
case h.h
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
x : PrimeSpectrum R
⊢ f ∈ ⨅ (_ : x ∈ t), x.asIdeal ↔ x ∈ t → f ∈ x.asIdeal

Proof state:
case h.h
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
f : R
x : PrimeSpectrum R
⊢ f ∈ ⨅ (_ : x ∈ t), x.asIdeal ↔ x ∈ t → f ∈ x.asIdeal

Tactic:
rw [Submodule.mem_iInf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem bmod_add_bdiv' (x : Int) (m : Nat) : bmod x m + bdiv x m * m = x

Proof state:
x : Int
m : Nat
⊢ x.bdiv m * ↑m + x.bmod m = x

Tactic:
exact bdiv_add_bmod' x m

Result:
no goals

Proof state:
x : Int
m : Nat
⊢ x.bmod m + x.bdiv m * ↑m = x

Tactic:
rw [Int.add_comm]

Result:
x : Int
m : Nat
⊢ x.bdiv m * ↑m + x.bmod m = x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldrM_cons [Monad m] [LawfulMonad m] (a : α) (l) (f : α → β → m β) (b) :
    (a :: l).foldrM f b = l.foldrM f b >>= f a

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
l : List α
f : α → β → m β
b : β
⊢ List.foldlM (fun s a => f a s) b (a :: l).reverse = List.foldlM (fun s a => f a s) b l.reverse >>= f a

Tactic:
induction l <;> simp_all

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
l : List α
f : α → β → m β
b : β
⊢ foldrM f b (a :: l) = foldrM f b l >>= f a

Tactic:
simp only [foldrM]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
l : List α
f : α → β → m β
b : β
⊢ List.foldlM (fun s a => f a s) b (a :: l).reverse = List.foldlM (fun s a => f a s) b l.reverse >>= f a
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_norm_eq_card (f : WithLp 0 (α × β)) :
    ‖f‖ = (if ‖f.fst‖ = 0 then 0 else 1) + (if ‖f.snd‖ = 0 then 0 else 1)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Norm α
inst✝ : Norm β
f : WithLp 0 (α × β)
⊢ ‖f‖ = (if ‖f.1‖ = 0 then 0 else 1) + if ‖f.2‖ = 0 then 0 else 1

Tactic:
convert if_pos rfl

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
/-- This lemma will be key to establishing good simp normal forms. -/
lemma map_mkPrecomp_eqToHom {F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v} {X Y : C} {f : X ⟶ Y}
    {g g' : yoneda.obj Y ⟶ A} (h : g = g') {x : F.obj (op (CostructuredArrow.mk g'))} :
    F.map (CostructuredArrow.mkPrecomp g f).op (F.map (eqToHom (by rw [h])) x) =
      F.map (eqToHom (by rw [h])) (F.map (CostructuredArrow.mkPrecomp g' f).op x)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
g g' : yoneda.obj Y ⟶ A
h : g = g'
x : F.obj (op (CostructuredArrow.mk g'))
⊢ F.map (CostructuredArrow.mkPrecomp g f).op (F.map (eqToHom ⋯) x) =
    F.map (eqToHom ⋯) (F.map (CostructuredArrow.mkPrecomp g' f).op x)

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
g g' : yoneda.obj Y ⟶ A
h : g = g'
x : F.obj (op (CostructuredArrow.mk g'))
⊢ op (CostructuredArrow.mk (yoneda.map f ≫ g')) = op (CostructuredArrow.mk (yoneda.map f ≫ g))

Tactic:
rw [h]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y : C
f : X ⟶ Y
g g' : yoneda.obj Y ⟶ A
h : g = g'
x : F.obj (op (CostructuredArrow.mk g'))
⊢ op (CostructuredArrow.mk g') = op (CostructuredArrow.mk g)

Tactic:
rw [h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addMap_of_Y_eq {P Q : Fin 3 → F} (hP : W.Nonsingular P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 = Q x * P z ^ 2)
    (hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3) : W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![1, 1, 0]⟧

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![1, 1, 0]⟧

Tactic:
by_cases hy : P y * Q z ^ 3 = Q y * P z ^ 3

Result:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : P y * Q z ^ 3 = Q y * P z ^ 3
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![1, 1, 0]⟧

case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : ¬P y * Q z ^ 3 = Q y * P z ^ 3
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![1, 1, 0]⟧

Proof state:
case pos
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : P y * Q z ^ 3 = Q y * P z ^ 3
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![1, 1, 0]⟧

Tactic:
rw [addMap_eq, add_of_Y_eq hPz hQz hx hy hy',
  smul_eq _ <| isUnit_dblU_of_Y_eq hP hPz hQz hx hy hy']

Result:
no goals

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 = Q x * P z ^ 2
hy' : P y * Q z ^ 3 = W.negY Q * P z ^ 3
hy : ¬P y * Q z ^ 3 = Q y * P z ^ 3
⊢ W.addMap ⟦P⟧ ⟦Q⟧ = ⟦![1, 1, 0]⟧

Tactic:
rw [addMap_eq, add_of_Y_ne hP.left hQ hPz hQz hx hy,
  smul_eq _ <| isUnit_addU_of_Y_ne hPz hQz hy]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem closedBall_eq_bInter_ball : closedBall x ε = ⋂ δ > ε, ball x δ

Proof state:
case h
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ (∀ ⦃c : ℝ⦄, ε < c → dist y x < c) ↔ ∀ i > ε, y ∈ ball x i

Tactic:
rfl

Result:
no goals

Proof state:
case h
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ y ∈ closedBall x ε ↔ y ∈ ⋂ δ, ⋂ (_ : δ > ε), ball x δ

Tactic:
rw [mem_closedBall, ← forall_lt_iff_le', mem_iInter₂]

Result:
case h
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ (∀ ⦃c : ℝ⦄, ε < c → dist y x < c) ↔ ∀ i > ε, y ∈ ball x i

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
⊢ closedBall x ε = ⋂ δ, ⋂ (_ : δ > ε), ball x δ

Tactic:
ext y

Result:
case h
α : Type u
inst✝ : PseudoMetricSpace α
x : α
ε : ℝ
y : α
⊢ y ∈ closedBall x ε ↔ y ∈ ⋂ δ, ⋂ (_ : δ > ε), ball x δ
-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem prod_apply_inr_fst (i) : (b.prod b' (Sum.inr i)).1 = 0 :=
  b.repr.injective <| by
    ext i
    simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply, LinearEquiv.prod_symm,
      LinearEquiv.prod_apply, b.repr.apply_symm_apply, LinearEquiv.symm_symm, repr_self,
      Equiv.toFun_as_coe, Finsupp.fst_sumFinsuppLEquivProdFinsupp, LinearEquiv.map_zero,
      Finsupp.zero_apply]
    apply Finsupp.single_eq_of_ne Sum.inr_ne_inl

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι'
⊢ b.repr ((b.prod b') (Sum.inr i)).1 = b.repr 0

Tactic:
ext i

Result:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i✝ : ι'
i : ι
⊢ (b.repr ((b.prod b') (Sum.inr i✝)).1) i = (b.repr 0) i

Proof state:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i✝ : ι'
i : ι
⊢ (b.repr ((b.prod b') (Sum.inr i✝)).1) i = (b.repr 0) i

Tactic:
simp only [Basis.prod, Basis.coe_ofRepr, LinearEquiv.symm_trans_apply, LinearEquiv.prod_symm,
  LinearEquiv.prod_apply, b.repr.apply_symm_apply, LinearEquiv.symm_symm, repr_self,
  Equiv.toFun_as_coe, Finsupp.fst_sumFinsuppLEquivProdFinsupp, LinearEquiv.map_zero,
  Finsupp.zero_apply]

Result:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i✝ : ι'
i : ι
⊢ (single (Sum.inr i✝) 1) (Sum.inl i) = 0

Proof state:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i✝ : ι'
i : ι
⊢ (single (Sum.inr i✝) 1) (Sum.inl i) = 0

Tactic:
apply Finsupp.single_eq_of_ne Sum.inr_ne_inl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem addCases_right {m n : Nat} {motive : Fin (m + n) → Sort _} {left right} (i : Fin n) :
    addCases (motive := motive) left right (natAdd m i) = right i

Proof state:
m n : Nat
motive : Fin (m + n) → Sort u_1
left : (i : Fin m) → motive (castAdd n i)
right : (i : Fin n) → motive (natAdd m i)
i : Fin n
this : ¬↑(natAdd m i) < m
⊢ HEq (right (subNat m (Fin.cast ⋯ (natAdd m i)) ⋯)) (right i)

Tactic:
congr 1

Result:
case e_1
m n : Nat
motive : Fin (m + n) → Sort u_1
left : (i : Fin m) → motive (castAdd n i)
right : (i : Fin n) → motive (natAdd m i)
i : Fin n
this : ¬↑(natAdd m i) < m
⊢ subNat m (Fin.cast ⋯ (natAdd m i)) ⋯ = i

Proof state:
m n : Nat
motive : Fin (m + n) → Sort u_1
left : (i : Fin m) → motive (castAdd n i)
right : (i : Fin n) → motive (natAdd m i)
i : Fin n
this : ¬↑(natAdd m i) < m
⊢ ⋯ ▸ right (subNat m (Fin.cast ⋯ (natAdd m i)) ⋯) = right i

Tactic:
exact eq_of_heq <| (eqRec_heq _ _).trans (by congr 1; simp)

Result:
no goals

Proof state:
m n : Nat
motive : Fin (m + n) → Sort u_1
left : (i : Fin m) → motive (castAdd n i)
right : (i : Fin n) → motive (natAdd m i)
i : Fin n
this : ¬↑(natAdd m i) < m
⊢ addCases left right (natAdd m i) = right i

Tactic:
rw [addCases, dif_neg this]

Result:
m n : Nat
motive : Fin (m + n) → Sort u_1
left : (i : Fin m) → motive (castAdd n i)
right : (i : Fin n) → motive (natAdd m i)
i : Fin n
this : ¬↑(natAdd m i) < m
⊢ ⋯ ▸ right (subNat m (Fin.cast ⋯ (natAdd m i)) ⋯) = right i

Proof state:
case e_1
m n : Nat
motive : Fin (m + n) → Sort u_1
left : (i : Fin m) → motive (castAdd n i)
right : (i : Fin n) → motive (natAdd m i)
i : Fin n
this : ¬↑(natAdd m i) < m
⊢ subNat m (Fin.cast ⋯ (natAdd m i)) ⋯ = i

Tactic:
simp

Result:
no goals

Proof state:
m n : Nat
motive : Fin (m + n) → Sort u_1
left : (i : Fin m) → motive (castAdd n i)
right : (i : Fin n) → motive (natAdd m i)
i : Fin n
⊢ addCases left right (natAdd m i) = right i

Tactic:
have : ¬(natAdd m i : Nat) < m := Nat.not_lt.2 (le_coe_natAdd ..)

Result:
m n : Nat
motive : Fin (m + n) → Sort u_1
left : (i : Fin m) → motive (castAdd n i)
right : (i : Fin n) → motive (natAdd m i)
i : Fin n
this : ¬↑(natAdd m i) < m
⊢ addCases left right (natAdd m i) = right i
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem foldr (f) (init : α) : ∀ {s}, ValidFor l m r s → s.foldr f init = m.foldr f init
  | _, ⟨⟩ => by simp [-List.append_assoc, Substring.foldr, foldrAux_of_valid]

Proof state:
α : Type u_1
l m r : List Char
f : Char → α → α
init : α
⊢ Substring.foldr f init
      { str := { data := l ++ m ++ r }, startPos := { byteIdx := utf8Len l },
        stopPos := { byteIdx := utf8Len l + utf8Len m } } =
    List.foldr f init m

Tactic:
simp [-List.append_assoc, Substring.foldr, foldrAux_of_valid]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
lemma Monotone.isCoboundedUnder_le_of_isCobounded {f : R → S} (f_incr : Monotone f)
    [NeBot F] (cobdd : IsCobounded (· ≤ ·) F) :
    F.IsCoboundedUnder (· ≤ ·) f

Proof state:
case intro
R : Type u_6
S : Type u_7
F : Filter R
inst✝² : LinearOrder R
inst✝¹ : LinearOrder S
f : R → S
f_incr : Monotone f
inst✝ : F.NeBot
cobdd : IsCobounded (fun x1 x2 => x1 ≤ x2) F
l : R
hl : ∃ᶠ (x : R) in F, l ≤ x
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f

Tactic:
exact IsCobounded.of_frequently_ge <| f_incr.frequently_ge_map_of_frequently_ge hl

Result:
no goals

Proof state:
R : Type u_6
S : Type u_7
F : Filter R
inst✝² : LinearOrder R
inst✝¹ : LinearOrder S
f : R → S
f_incr : Monotone f
inst✝ : F.NeBot
cobdd : IsCobounded (fun x1 x2 => x1 ≤ x2) F
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f

Tactic:
obtain ⟨l, hl⟩ := IsCobounded.frequently_ge cobdd

Result:
case intro
R : Type u_6
S : Type u_7
F : Filter R
inst✝² : LinearOrder R
inst✝¹ : LinearOrder S
f : R → S
f_incr : Monotone f
inst✝ : F.NeBot
cobdd : IsCobounded (fun x1 x2 => x1 ≤ x2) F
l : R
hl : ∃ᶠ (x : R) in F, l ≤ x
⊢ IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f
-- Mathlib/RepresentationTheory/GroupCohomology/Basic.lean
theorem d_eq :
    d n A =
      ((diagonalHomEquiv n A).toModuleIso.inv ≫
        (linearYonedaObjResolution A).d n (n + 1) ≫
          (diagonalHomEquiv (n + 1) A).toModuleIso.hom).hom

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
⊢ (d n A) f g =
    (ModuleCat.Hom.hom
        ((diagonalHomEquiv n A).toModuleIso.inv ≫
          (linearYonedaObjResolution A).d n (n + 1) ≫ (diagonalHomEquiv (n + 1) A).toModuleIso.hom))
      f g

Tactic:
change d n A f g = diagonalHomEquiv (n + 1) A
  ((resolution k G).d (n + 1) n ≫ (diagonalHomEquiv n A).symm f) g

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
⊢ (d n A) f g = (diagonalHomEquiv (n + 1) A) ((resolution k G).d (n + 1) n ≫ (diagonalHomEquiv n A).symm f) g

Proof state:
case h.h.e_a.e_f.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
x : Fin (n + 1)
⊢ (-1) ^ (↑x + 1) • f (x.contractNth (fun x1 x2 => x1 * x2) g) =
    (ConcreteCategory.hom ((diagonalHomEquiv n A).symm f).hom)
      ((-1) ^ ↑x.succ • Finsupp.single (Fin.partialProd g ∘ x.succ.succAbove) 1)

Tactic:
erw [map_smul, diagonalHomEquiv_symm_partialProd_succ, Fin.val_succ]

Result:
no goals

Proof state:
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
⊢ (d n A) f g =
    (ConcreteCategory.hom ((diagonalHomEquiv n A).symm f).hom)
      (∑ p : Fin (n + 1 + 1), Finsupp.single (Fin.partialProd g ∘ p.succAbove) ((-1) ^ ↑p))

Tactic:
simp only [map_sum, ← Finsupp.smul_single_one _ ((-1 : k) ^ _)]

Result:
case h.h
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
A : Rep k G
f : (Fin n → G) → ↑A.V
g : Fin (n + 1) → G
⊢ (d n A) f g =
    ∑ x : Fin (n + 1 + 1),
      (ConcreteCategory.hom ((diagonalHomEquiv n A).symm f).hom)
        ((-1) ^ ↑x • Finsupp.single (Fin.partialProd g ∘ x.succAbove) 1)
-- Mathlib/Data/List/Sort.lean
theorem orderedInsert_length : ∀ (L : List α) (a : α), (L.orderedInsert r a).length = L.length + 1
  | [], _ => rfl
  | hd :: tl, a => by
    dsimp [orderedInsert]
    split_ifs <;> simp [orderedInsert_length tl]

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
hd : α
tl : List α
a : α
⊢ (orderedInsert r a (hd :: tl)).length = (hd :: tl).length + 1

Tactic:
dsimp [orderedInsert]

Result:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
hd : α
tl : List α
a : α
⊢ (if r a hd then a :: hd :: tl else hd :: orderedInsert r a tl).length = tl.length + 1 + 1

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
hd : α
tl : List α
a : α
⊢ (if r a hd then a :: hd :: tl else hd :: orderedInsert r a tl).length = tl.length + 1 + 1

Tactic:
split_ifs <;> simp [orderedInsert_length tl]

Result:
no goals