harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem shiftRight_eq_ushiftRightRec (x : BitVec w₁) (y : BitVec w₂) :
    x >>> y = ushiftRightRec x y (w₂ - 1)

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
⊢ x >>> y = x.ushiftRightRec y (w₂ - 1)

Tactic:
rcases w₂ with rfl | w₂

Result:
case zero
w₁ : Nat
x : BitVec w₁
y : BitVec 0
⊢ x >>> y = x.ushiftRightRec y (0 - 1)

case succ
w₁ : Nat
x : BitVec w₁
w₂ : Nat
y : BitVec (w₂ + 1)
⊢ x >>> y = x.ushiftRightRec y (w₂ + 1 - 1)

Proof state:
case succ
w₁ : Nat
x : BitVec w₁
w₂ : Nat
y : BitVec (w₂ + 1)
⊢ x >>> y = x.ushiftRightRec y (w₂ + 1 - 1)

Tactic:
simp [ushiftRightRec_eq]

Result:
no goals

Proof state:
case zero
w₁ : Nat
x : BitVec w₁
y : BitVec 0
⊢ x >>> y = x.ushiftRightRec y (0 - 1)

Tactic:
simp [of_length_zero]

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem eq_pell {x y : ℕ} (hp : x * x - d a1 * y * y = 1) : ∃ n, x = xn a1 n ∧ y = yn a1 n :=
  have : (1 : ℤ√(d a1)) ≤ ⟨x, y⟩ :=
    match x, hp with
    | 0, (hp : 0 - _ = 1) => by rw [zero_tsub] at hp; contradiction
    | x + 1, _hp =>
      Zsqrtd.le_of_le_le (Int.ofNat_le_ofNat_of_le <| Nat.succ_pos x) (Int.ofNat_zero_le _)
  let ⟨m, e⟩ := eq_pellZd a1 ⟨x, y⟩ this ((isPell_nat a1).2 hp)
  ⟨m,
    match x, y, e with
    | _, _, rfl => ⟨rfl, rfl⟩⟩

Proof state:
a : ℕ
a1 : 1 < a
x y : ℕ
hp✝ : x * x - Pell.d a1 * y * y = 1
hp : 0 - Pell.d a1 * y * y = 1
⊢ 1 ≤ { re := ↑0, im := ↑y }

Tactic:
rw [zero_tsub] at hp

Result:
a : ℕ
a1 : 1 < a
x y : ℕ
hp✝ : x * x - Pell.d a1 * y * y = 1
hp : 0 = 1
⊢ 1 ≤ { re := ↑0, im := ↑y }

Proof state:
a : ℕ
a1 : 1 < a
x y : ℕ
hp✝ : x * x - Pell.d a1 * y * y = 1
hp : 0 = 1
⊢ 1 ≤ { re := ↑0, im := ↑y }

Tactic:
contradiction

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_congr [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {a b : α}
    (h : a == b) : getValue? a l = getValue? b l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
a b : α
h : (a == b) = true
⊢ getValue? a l = getValue? b l

Tactic:
simp [getValue?_eq_getEntry?, getEntry?_congr h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem ite_eq_cond_iff {p : Prop} {a : Bool} [h : Decidable p] {x y u v : α} :
  (ite p x y = cond a u v) ↔ ite p x y = ite a u v

Proof state:
α : Type u_1
p : Prop
a : Bool
h : Decidable p
x y u v : α
⊢ ((if p then x else y) = bif a then u else v) ↔ (if p then x else y) = if a = true then u else v

Tactic:
simp [Bool.cond_eq_ite]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_inj {a b : Array α} : a.toList = b.toList ↔ a = b

Proof state:
case mk.mk
α : Type u_1
toList✝¹ toList✝ : List α
⊢ { toList := toList✝¹ }.toList = { toList := toList✝ }.toList ↔ { toList := toList✝¹ } = { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
b : Array α
toList✝ : List α
⊢ { toList := toList✝ }.toList = b.toList ↔ { toList := toList✝ } = b

Tactic:
cases b

Result:
case mk.mk
α : Type u_1
toList✝¹ toList✝ : List α
⊢ { toList := toList✝¹ }.toList = { toList := toList✝ }.toList ↔ { toList := toList✝¹ } = { toList := toList✝ }

Proof state:
α : Type u_1
a b : Array α
⊢ a.toList = b.toList ↔ a = b

Tactic:
cases a

Result:
case mk
α : Type u_1
b : Array α
toList✝ : List α
⊢ { toList := toList✝ }.toList = b.toList ↔ { toList := toList✝ } = b
-- Mathlib/CategoryTheory/Adjunction/Reflective.lean
lemma counit_obj_eq_map_counit [Coreflective j] (X : D) :
    (coreflectorAdjunction j).counit.app (j.obj ((coreflector j).obj X)) =
      j.map ((coreflector j).map ((coreflectorAdjunction j).counit.app X))

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
j : C ⥤ D
inst✝ : Coreflective j
X : D
⊢ j.map ((coreflectorAdjunction j).unit.app ((coreflector j).obj X)) ≫
      (coreflectorAdjunction j).counit.app (j.obj ((coreflector j).obj X)) =
    j.map
      ((coreflectorAdjunction j).unit.app ((coreflector j).obj X) ≫
        (coreflector j).map ((coreflectorAdjunction j).counit.app X))

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
j : C ⥤ D
inst✝ : Coreflective j
X : D
⊢ (coreflectorAdjunction j).counit.app (j.obj ((coreflector j).obj X)) =
    j.map ((coreflector j).map ((coreflectorAdjunction j).counit.app X))

Tactic:
rw [← cancel_epi (j.map ((coreflectorAdjunction j).unit.app ((coreflector j).obj X))),
  ← j.map_comp]

Result:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
j : C ⥤ D
inst✝ : Coreflective j
X : D
⊢ j.map ((coreflectorAdjunction j).unit.app ((coreflector j).obj X)) ≫
      (coreflectorAdjunction j).counit.app (j.obj ((coreflector j).obj X)) =
    j.map
      ((coreflectorAdjunction j).unit.app ((coreflector j).obj X) ≫
        (coreflector j).map ((coreflectorAdjunction j).counit.app X))
-- Mathlib/Algebra/Order/UpperLower.lean
theorem upperClosure_mul : ↑(upperClosure s) * t = upperClosure (s * t)

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
⊢ t * ↑(upperClosure s) = ↑(upperClosure (t * s))

Tactic:
exact mul_upperClosure _ _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
⊢ ↑(upperClosure s) * t = ↑(upperClosure (s * t))

Tactic:
simp_rw [mul_comm _ t]

Result:
α : Type u_1
inst✝ : OrderedCommGroup α
s t : Set α
⊢ t * ↑(upperClosure s) = ↑(upperClosure (t * s))
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem uniformContinuous_restrict_toFun :
    UniformContinuous ((⋃₀ 𝔖).restrict ∘ toFun 𝔖 : (α →ᵤ[𝔖] β) → ⋃₀ 𝔖 → β)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
x : α
hx : x ∈ ⋃₀ 𝔖
s : Set α
hs : s ∈ 𝔖
hxs : x ∈ s
⊢ UniformContinuous fun x_1 => ((⋃₀ 𝔖).restrict ∘ ⇑(toFun 𝔖)) x_1 ⟨x, hx⟩

Tactic:
exact uniformContinuous_eval_of_mem β 𝔖 hxs hs

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ UniformContinuous ((⋃₀ 𝔖).restrict ∘ ⇑(toFun 𝔖))

Tactic:
rw [uniformContinuous_pi]

Result:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ ∀ (i : ↑(⋃₀ 𝔖)), UniformContinuous fun x => ((⋃₀ 𝔖).restrict ∘ ⇑(toFun 𝔖)) x i

Proof state:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
x : α
hx : x ∈ ⋃₀ 𝔖
⊢ UniformContinuous fun x_1 => ((⋃₀ 𝔖).restrict ∘ ⇑(toFun 𝔖)) x_1 ⟨x, hx⟩

Tactic:
obtain ⟨s : Set α, hs : s ∈ 𝔖, hxs : x ∈ s⟩ := mem_sUnion.mpr hx

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
x : α
hx : x ∈ ⋃₀ 𝔖
s : Set α
hs : s ∈ 𝔖
hxs : x ∈ s
⊢ UniformContinuous fun x_1 => ((⋃₀ 𝔖).restrict ∘ ⇑(toFun 𝔖)) x_1 ⟨x, hx⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ ∀ (i : ↑(⋃₀ 𝔖)), UniformContinuous fun x => ((⋃₀ 𝔖).restrict ∘ ⇑(toFun 𝔖)) x i

Tactic:
intro ⟨x, hx⟩

Result:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
x : α
hx : x ∈ ⋃₀ 𝔖
⊢ UniformContinuous fun x_1 => ((⋃₀ 𝔖).restrict ∘ ⇑(toFun 𝔖)) x_1 ⟨x, hx⟩
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem flatten_replicate_singleton : (replicate n [a]).flatten = replicate n a

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
⊢ (replicate n [a]).flatten = replicate n a

Tactic:
induction n <;> simp_all [replicate_succ]

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
@[simp]
lemma toMvPolynomial_id : (id : M₁ →ₗ[R] M₁).toMvPolynomial b₁ b₁ = X

Proof state:
R : Type u_1
M₁ : Type u_2
ι₁ : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : Fintype ι₁
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
⊢ toMvPolynomial b₁ b₁ id = X

Tactic:
unfold toMvPolynomial

Result:
R : Type u_1
M₁ : Type u_2
ι₁ : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : Fintype ι₁
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
⊢ (fun i => ((toMatrix b₁ b₁) id).toMvPolynomial i) = X

Proof state:
R : Type u_1
M₁ : Type u_2
ι₁ : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M₁
inst✝² : Module R M₁
inst✝¹ : Fintype ι₁
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
⊢ (fun i => ((toMatrix b₁ b₁) id).toMvPolynomial i) = X

Tactic:
simp only [toMatrix_id, Matrix.toMvPolynomial_one]

Result:
no goals
-- Mathlib/Order/Defs/LinearOrder.lean
lemma lt_min (h₁ : a < b) (h₂ : a < c) : a < min b c

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : a < b
h₂ : a < c
⊢ a < min b c

Tactic:
cases le_total b c <;> simp [min_eq_left, min_eq_right, *]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem partialProd_left_inv {G : Type*} [Group G] (f : Fin (n + 1) → G) :
    (f 0 • partialProd fun i : Fin n => (f i)⁻¹ * f i.succ) = f :=
  funext fun x => Fin.inductionOn x (by simp) fun x hx => by
    simp only [coe_eq_castSucc, Pi.smul_apply, smul_eq_mul] at hx ⊢
    rw [partialProd_succ, ← mul_assoc, hx, mul_inv_cancel_left]

Proof state:
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin (n + 1) → G
x✝ : Fin (n + 1)
x : Fin n
hx : f 0 * partialProd (fun i => (f i.castSucc)⁻¹ * f i.succ) x.castSucc = f x.castSucc
⊢ f 0 * partialProd (fun i => (f i.castSucc)⁻¹ * f i.succ) x.succ = f x.succ

Tactic:
rw [partialProd_succ, ← mul_assoc, hx, mul_inv_cancel_left]

Result:
no goals

Proof state:
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin (n + 1) → G
x✝ : Fin (n + 1)
x : Fin n
hx : (f 0 • partialProd fun i => (f ↑↑i)⁻¹ * f i.succ) x.castSucc = f x.castSucc
⊢ (f 0 • partialProd fun i => (f ↑↑i)⁻¹ * f i.succ) x.succ = f x.succ

Tactic:
simp only [coe_eq_castSucc, Pi.smul_apply, smul_eq_mul] at hx ⊢

Result:
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin (n + 1) → G
x✝ : Fin (n + 1)
x : Fin n
hx : f 0 * partialProd (fun i => (f i.castSucc)⁻¹ * f i.succ) x.castSucc = f x.castSucc
⊢ f 0 * partialProd (fun i => (f i.castSucc)⁻¹ * f i.succ) x.succ = f x.succ

Proof state:
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin (n + 1) → G
x : Fin (n + 1)
⊢ (f 0 • partialProd fun i => (f ↑↑i)⁻¹ * f i.succ) 0 = f 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem swap_swap (x : α ⊕ β) : swap (swap x) = x

Proof state:
α : Type u_1
β : Type u_2
x : α ⊕ β
⊢ x.swap.swap = x

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/Analysis/Seminorm.lean
theorem iSup_apply {ι : Sort*} {p : ι → Seminorm 𝕜 E}
    (hp : BddAbove (range p)) {x : E} : (⨆ i, p i) x = ⨆ i, p i x

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
ι : Sort u_12
p : ι → Seminorm 𝕜 E
hp : BddAbove (range p)
x : E
⊢ (⨆ i, p i) x = ⨆ i, (p i) x

Tactic:
rw [Seminorm.coe_iSup_eq hp, iSup_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Classical.lean
theorem decide_not (p : Prop) [Decidable (¬ p)] : decide (¬p) = !decide p :=
  byCases (fun h : p => by simp_all) (fun h => by simp_all)

Proof state:
p : Prop
inst✝ : Decidable ¬p
h : p
⊢ (decide ¬p) = !decide p

Tactic:
simp_all

Result:
no goals

Proof state:
p : Prop
inst✝ : Decidable ¬p
h : ¬p
⊢ (decide ¬p) = !decide p

Tactic:
simp_all

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Comma.lean
@[ext]
lemma Over.Hom.ext {A B : P.Over Q X} {f g : A ⟶ B} (h : f.left = g.left) : f = g

Proof state:
case h.h₁
T : Type u_1
inst✝¹ : Category.{u_2, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Over Q X
f g : A ⟶ B
h : f.left = g.left
⊢ (Comma.Hom.hom f).left = (Comma.Hom.hom g).left

Tactic:
exact h

Result:
no goals

Proof state:
T : Type u_1
inst✝¹ : Category.{u_2, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Over Q X
f g : A ⟶ B
h : f.left = g.left
⊢ f = g

Tactic:
ext

Result:
case h.h₁
T : Type u_1
inst✝¹ : Category.{u_2, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Over Q X
f g : A ⟶ B
h : f.left = g.left
⊢ (Comma.Hom.hom f).left = (Comma.Hom.hom g).left

case h.h₂
T : Type u_1
inst✝¹ : Category.{u_2, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Over Q X
f g : A ⟶ B
h : f.left = g.left
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right

Proof state:
case h.h₂
T : Type u_1
inst✝¹ : Category.{u_2, u_1} T
P Q : MorphismProperty T
X : T
inst✝ : Q.IsMultiplicative
A B : P.Over Q X
f g : A ⟶ B
h : f.left = g.left
⊢ (Comma.Hom.hom f).right = (Comma.Hom.hom g).right

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma limitRightOpIsoOpColimit_inv_comp_π (F : Jᵒᵖ ⥤ C) [HasColimit F] (j : J) :
    (limitRightOpIsoOpColimit F).inv ≫ limit.π F.rightOp j = (colimit.ι F (op j)).op

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : Jᵒᵖ ⥤ C
inst✝ : HasColimit F
j : J
⊢ (limitRightOpIsoOpColimit F).inv ≫ limit.π F.rightOp j = (colimit.ι F (op j)).op

Tactic:
simp [limitRightOpIsoOpColimit]

Result:
no goals
-- Mathlib/Algebra/Polynomial/RingDivision.lean
theorem Monic.prime_of_degree_eq_one (hp1 : degree p = 1) (hm : Monic p) : Prime p :=
  have : p = X - C (-p.coeff 0)

Proof state:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
hp1 : p.degree = 1
hm : p.Monic
⊢ p = X - C (-p.coeff 0)

Tactic:
simpa [hm.leadingCoeff] using eq_X_add_C_of_degree_eq_one hp1

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_one : m.degree (1 : MvPolynomial σ R) = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ (if 1 = 0 then 0 else 0) = 0

Tactic:
simp

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
⊢ m.degree 1 = 0

Tactic:
nontriviality R

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ m.degree 1 = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ m.degree 1 = 0

Tactic:
rw [MvPolynomial.one_def, degree_monomial]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ (if 1 = 0 then 0 else 0) = 0

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ m.degree 1 = 0

Tactic:
classical rw [MvPolynomial.one_def, degree_monomial]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ (if 1 = 0 then 0 else 0) = 0
-- Mathlib/Topology/VectorBundle/Constructions.lean
theorem trivialization.coordChangeL (b : B) :
    (trivialization B F).coordChangeL 𝕜 (trivialization B F) b =
      ContinuousLinearEquiv.refl 𝕜 F

Proof state:
case h.h
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
v : F
⊢ (↑(trivialization B F) (↑(trivialization B F).symm (b, v))).2 = (ContinuousLinearEquiv.refl 𝕜 F) v

case h.h.hb
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
v : F
⊢ b ∈ (trivialization B F).baseSet ∩ (trivialization B F).baseSet

Tactic:
exacts [rfl, ⟨mem_univ _, mem_univ _⟩]

Result:
no goals

Proof state:
case h.h
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
v : F
⊢ (Trivialization.coordChangeL 𝕜 (trivialization B F) (trivialization B F) b) v = (ContinuousLinearEquiv.refl 𝕜 F) v

Tactic:
rw [Trivialization.coordChangeL_apply']

Result:
case h.h
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
v : F
⊢ (↑(trivialization B F) (↑(trivialization B F).symm (b, v))).2 = (ContinuousLinearEquiv.refl 𝕜 F) v

case h.h.hb
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
v : F
⊢ b ∈ (trivialization B F).baseSet ∩ (trivialization B F).baseSet

Proof state:
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
⊢ Trivialization.coordChangeL 𝕜 (trivialization B F) (trivialization B F) b = ContinuousLinearEquiv.refl 𝕜 F

Tactic:
ext v

Result:
case h.h
𝕜 : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : TopologicalSpace B
b : B
v : F
⊢ (Trivialization.coordChangeL 𝕜 (trivialization B F) (trivialization B F) b) v = (ContinuousLinearEquiv.refl 𝕜 F) v
-- Mathlib/Algebra/Homology/TotalComplex.lean
@[reassoc (attr := simp)]
lemma d₂_mapMap (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) :
    K.d₂ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) _ i₁₂ =
    (φ.f i₁).f i₂ ≫ L.d₂ c₁₂ i₁ i₂ i₁₂

Proof state:
case neg
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₂ c₁₂ i₁ i₂ i₁₂

Tactic:
simp [d₂_eq_zero _ c₁₂ i₁ i₂ i₁₂ h]

Result:
no goals

Proof state:
case pos
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₂ c₁₂ i₁ i₂ i₁₂

Tactic:
simp [totalAux.d₂_eq' _ c₁₂ i₁ h]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₂ c₁₂ i₁ i₂ i₁₂

Tactic:
by_cases h : c₂.Rel i₂ (c₂.next i₂)

Result:
case pos
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₂ c₁₂ i₁ i₂ i₁₂

case neg
C : Type u_1
inst✝⁵ : Category.{u_5, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ ≫ GradedObject.mapMap (toGradedObjectMap φ) (c₁.π c₂ c₁₂) i₁₂ = (φ.f i₁).f i₂ ≫ L.d₂ c₁₂ i₁ i₂ i₁₂
-- Mathlib/CategoryTheory/Abelian/Exact.lean
theorem exact_cokernel {X Y : C} (f : X ⟶ Y) :
    (ShortComplex.mk f (cokernel.π f) (by simp)).Exact :=
  exact_of_g_is_cokernel _ (cokernelIsCokernel f)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
X Y : C
f : X ⟶ Y
⊢ f ≫ cokernel.π f = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem AnalyticAt.contDiffAt [CompleteSpace F] (h : AnalyticAt 𝕜 f x) :
    ContDiffAt 𝕜 n f x

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
x : E
n : WithTop ℕ∞
inst✝ : CompleteSpace F
h : AnalyticAt 𝕜 f x
⊢ ContDiffWithinAt 𝕜 n f univ x

Tactic:
rw [← analyticWithinAt_univ] at h

Result:
𝕜 : 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
x : E
n : WithTop ℕ∞
inst✝ : CompleteSpace F
h : AnalyticWithinAt 𝕜 f univ x
⊢ ContDiffWithinAt 𝕜 n f univ x

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
x : E
n : WithTop ℕ∞
inst✝ : CompleteSpace F
h : AnalyticWithinAt 𝕜 f univ x
⊢ ContDiffWithinAt 𝕜 n f univ x

Tactic:
exact h.contDiffWithinAt

Result:
no goals

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
x : E
n : WithTop ℕ∞
inst✝ : CompleteSpace F
h : AnalyticAt 𝕜 f x
⊢ ContDiffAt 𝕜 n f x

Tactic:
rw [← contDiffWithinAt_univ]

Result:
𝕜 : 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
x : E
n : WithTop ℕ∞
inst✝ : CompleteSpace F
h : AnalyticAt 𝕜 f x
⊢ ContDiffWithinAt 𝕜 n f univ x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldl_flip_cons_eq_append (l : List α) : l.foldl (fun x y => y :: x) l' = l.reverse ++ l'

Proof state:
α : Type u_1
l' l : List α
⊢ foldl (fun x y => y :: x) l' l = l.reverse ++ l'

Tactic:
induction l generalizing l' <;> simp [*]

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive]
lemma isMulFreimanHom_const {b : β} (hb : b ∈ B) : IsMulFreimanHom n A B fun _ ↦ b where
  mapsTo _ _ := hb
  map_prod_eq_map_prod s t _ _ hs ht _

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
n : ℕ
b : β
hb : b ∈ B
s t : Multiset α
x✝² : ∀ ⦃x : α⦄, x ∈ s → x ∈ A
x✝¹ : ∀ ⦃x : α⦄, x ∈ t → x ∈ A
hs : s.card = n
ht : t.card = n
x✝ : s.prod = t.prod
⊢ (map (fun x => b) s).prod = (map (fun x => b) t).prod

Tactic:
simp only [map_const', hs, prod_replicate, ht]

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem elim_none_some (f : Option α → β) : (fun x ↦ Option.elim x (f none) (f ∘ some)) = f :=
  funext fun o ↦ by cases o <;> rfl

Proof state:
α : Type u_1
β : Type u_2
f : Option α → β
o : Option α
⊢ o.elim (f none) (f ∘ some) = f o

Tactic:
cases o <;> rfl

Result:
no goals