harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/AbelianImages.lean
theorem PreservesCoimage.factorThruCoimage_iso_inv :
    (PreservesCoimage.iso F f).inv ≫ F.map (Abelian.factorThruCoimage f)  =
      Abelian.factorThruCoimage (F.map f)

Proof state:
case h
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasKernels C
inst✝⁷ : HasCokernels C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
inst✝⁴ : HasKernels D
inst✝³ : HasCokernels D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair F
inst✝ : PreservesColimitsOfShape WalkingParallelPair F
X Y : C
f : X ⟶ Y
⊢ coequalizer.π (kernel.ι (F.map f)) 0 ≫ (iso F f).inv ≫ F.map (Abelian.factorThruCoimage f) =
    coequalizer.π (kernel.ι (F.map f)) 0 ≫ Abelian.factorThruCoimage (F.map f)

Tactic:
simp [iso]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasKernels C
inst✝⁷ : HasCokernels C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
inst✝⁴ : HasKernels D
inst✝³ : HasCokernels D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair F
inst✝ : PreservesColimitsOfShape WalkingParallelPair F
X Y : C
f : X ⟶ Y
⊢ (iso F f).inv ≫ F.map (Abelian.factorThruCoimage f) = Abelian.factorThruCoimage (F.map f)

Tactic:
ext

Result:
case h
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasKernels C
inst✝⁷ : HasCokernels C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
inst✝⁴ : HasKernels D
inst✝³ : HasCokernels D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair F
inst✝ : PreservesColimitsOfShape WalkingParallelPair F
X Y : C
f : X ⟶ Y
⊢ coequalizer.π (kernel.ι (F.map f)) 0 ≫ (iso F f).inv ≫ F.map (Abelian.factorThruCoimage f) =
    coequalizer.π (kernel.ι (F.map f)) 0 ≫ Abelian.factorThruCoimage (F.map f)
-- Mathlib/FieldTheory/Extension.lean
theorem exists_lift_of_splits' (x : Lifts F E K) {s : E} (h1 : IsIntegral x.carrier s)
    (h2 : (minpoly x.carrier s).Splits x.emb.toRingHom) : ∃ y, x ≤ y ∧ s ∈ y.carrier :=
  have I2 := (minpoly.degree_pos h1).ne'
  letI : Algebra x.carrier K := x.emb.toRingHom.toAlgebra
  let carrier := x.carrier⟮s⟯.restrictScalars F
  letI : Algebra x.carrier carrier := x.carrier⟮s⟯.toSubalgebra.algebra
  let φ : carrier →ₐ[x.carrier] K := ((algHomAdjoinIntegralEquiv x.carrier h1).symm
    ⟨rootOfSplits x.emb.toRingHom h2 I2, by
      rw [mem_aroots, and_iff_right (minpoly.ne_zero h1)]
      exact map_rootOfSplits x.emb.toRingHom h2 I2⟩)
  ⟨⟨carrier, (@algHomEquivSigma F x.carrier carrier K _ _ _ _ _ _ _ _
      (IsScalarTower.of_algebraMap_eq fun _ ↦ rfl)).symm ⟨x.emb, φ⟩⟩,
    ⟨fun z hz ↦ algebraMap_mem x.carrier⟮s⟯ ⟨z, hz⟩, φ.commutes⟩,
    mem_adjoin_simple_self x.carrier s⟩

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
x : Lifts F E K
s : E
h1 : IsIntegral (↥x.carrier) s
h2 : Splits x.emb.toRingHom (minpoly (↥x.carrier) s)
I2 : (minpoly (↥x.carrier) s).degree ≠ 0
this✝ : Algebra (↥x.carrier) K := x.emb.toAlgebra
carrier : IntermediateField F E := restrictScalars F (↥x.carrier)⟮s⟯
this : Algebra ↥x.carrier ↥carrier := (↥x.carrier)⟮s⟯.algebra
⊢ rootOfSplits x.emb.toRingHom h2 I2 ∈ (minpoly (↥x.carrier) s).aroots K

Tactic:
rw [mem_aroots, and_iff_right (minpoly.ne_zero h1)]

Result:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
x : Lifts F E K
s : E
h1 : IsIntegral (↥x.carrier) s
h2 : Splits x.emb.toRingHom (minpoly (↥x.carrier) s)
I2 : (minpoly (↥x.carrier) s).degree ≠ 0
this✝ : Algebra (↥x.carrier) K := x.emb.toAlgebra
carrier : IntermediateField F E := restrictScalars F (↥x.carrier)⟮s⟯
this : Algebra ↥x.carrier ↥carrier := (↥x.carrier)⟮s⟯.algebra
⊢ (aeval (rootOfSplits x.emb.toRingHom h2 I2)) (minpoly (↥x.carrier) s) = 0

Proof state:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Field K
inst✝¹ : Algebra F E
inst✝ : Algebra F K
x : Lifts F E K
s : E
h1 : IsIntegral (↥x.carrier) s
h2 : Splits x.emb.toRingHom (minpoly (↥x.carrier) s)
I2 : (minpoly (↥x.carrier) s).degree ≠ 0
this✝ : Algebra (↥x.carrier) K := x.emb.toAlgebra
carrier : IntermediateField F E := restrictScalars F (↥x.carrier)⟮s⟯
this : Algebra ↥x.carrier ↥carrier := (↥x.carrier)⟮s⟯.algebra
⊢ (aeval (rootOfSplits x.emb.toRingHom h2 I2)) (minpoly (↥x.carrier) s) = 0

Tactic:
exact map_rootOfSplits x.emb.toRingHom h2 I2

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le.dest {a b : Int} (h : a ≤ b) : ∃ n : Nat, a + n = b :=
  let ⟨n, h₁⟩ := le.dest_sub h
  ⟨n, by rw [← h₁, Int.add_comm]; simp [Int.sub_eq_add_neg, Int.add_assoc]⟩

Proof state:
a b : Int
h : a ≤ b
n : Nat
h₁ : b - a = ↑n
⊢ a + ↑n = b

Tactic:
rw [← h₁, Int.add_comm]

Result:
a b : Int
h : a ≤ b
n : Nat
h₁ : b - a = ↑n
⊢ b - a + a = b

Proof state:
a b : Int
h : a ≤ b
n : Nat
h₁ : b - a = ↑n
⊢ b - a + a = b

Tactic:
simp [Int.sub_eq_add_neg, Int.add_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem eq_true_eq_id : Eq True = id

Proof state:
⊢ Eq True = id

Tactic:
funext _

Result:
case h
x✝ : Prop
⊢ (True = x✝) = id x✝

Proof state:
case h
x✝ : Prop
⊢ (True = x✝) = id x✝

Tactic:
simp only [true_iff, id_def, eq_iff_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem reverse_inj {xs ys : Array α} : xs.reverse = ys.reverse ↔ xs = ys

Proof state:
α : Type u_1
xs ys : Array α
⊢ xs.reverse = ys.reverse ↔ xs = ys

Tactic:
simp [reverse_eq_iff]

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem StrictConvexOn.congr (hf : StrictConvexOn 𝕜 s f) (hfg : EqOn f g s) :
    StrictConvexOn 𝕜 s g :=
  ⟨hf.1, fun x hx y hy hxy a b ha hb hab => by
    simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha.le hb.le hab)] using
      hf.2 hx hy hxy ha hb hab⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : SMul 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hfg : EqOn f g s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ g (a • x + b • y) < a • g x + b • g y

Tactic:
simpa only [← hfg hx, ← hfg hy, ← hfg (hf.1 hx hy ha.le hb.le hab)] using
  hf.2 hx hy hxy ha hb hab

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
lemma exists_card_eq [Infinite α] : ∀ n : ℕ, ∃ s : Finset α, s.card = n
  | 0 => ⟨∅, card_empty⟩
  | n + 1 => by
    classical
    obtain ⟨s, rfl⟩ := exists_card_eq n
    obtain ⟨a, ha⟩ := s.exists_not_mem
    exact ⟨insert a s, card_insert_of_not_mem ha⟩

Proof state:
case intro
α : Type u
inst✝ : Infinite α
s : Finset α
⊢ ∃ s_1, #s_1 = #s + 1

Tactic:
obtain ⟨a, ha⟩ := s.exists_not_mem

Result:
case intro.intro
α : Type u
inst✝ : Infinite α
s : Finset α
a : α
ha : a ∉ s
⊢ ∃ s_1, #s_1 = #s + 1

Proof state:
α : Type u
inst✝ : Infinite α
n : ℕ
⊢ ∃ s, #s = n + 1

Tactic:
classical
obtain ⟨s, rfl⟩ := exists_card_eq n
obtain ⟨a, ha⟩ := s.exists_not_mem
exact ⟨insert a s, card_insert_of_not_mem ha⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : Infinite α
n : ℕ
⊢ ∃ s, #s = n + 1

Tactic:
obtain ⟨s, rfl⟩ := exists_card_eq n

Result:
case intro
α : Type u
inst✝ : Infinite α
s : Finset α
⊢ ∃ s_1, #s_1 = #s + 1

Proof state:
case intro.intro
α : Type u
inst✝ : Infinite α
s : Finset α
a : α
ha : a ∉ s
⊢ ∃ s_1, #s_1 = #s + 1

Tactic:
exact ⟨insert a s, card_insert_of_not_mem ha⟩

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleNumber.lean
theorem remainder_summable {m : ℝ} (hm : 1 < m) (k : ℕ) :
    Summable fun i : ℕ => 1 / m ^ (i + (k + 1))!

Proof state:
m : ℝ
hm : 1 < m
k : ℕ
⊢ Summable fun i => 1 / m ^ (i + (k + 1))!

Tactic:
convert (summable_nat_add_iff (k + 1)).2 (LiouvilleNumber.summable hm)

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
@[simp]
lemma homMk₅_app_three :
    (homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app ⟨3, by valid⟩ = app₃ := rfl

Proof state:
C : Type u_1
inst✝ : Category.{?u.364788, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 5
app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯
app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯
app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯
app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯
app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯
app₅ : f.obj' 5 ⋯ ⟶ g.obj' 5 ⋯
w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯
w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯
w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃ = app₂ ≫ g.map' 2 3 ⋯ ⋯
w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄ = app₃ ≫ g.map' 3 4 ⋯ ⋯
w₄ : f.map' 4 5 ⋯ ⋯ ≫ app₅ = app₄ ≫ g.map' 4 5 ⋯ ⋯
⊢ 3 < 5 + 1

Tactic:
valid

Result:
no goals
-- Mathlib/Data/Multiset/Basic.lean
theorem mem_toList {a : α} {s : Multiset α} : a ∈ s.toList ↔ a ∈ s

Proof state:
α : Type u_1
a : α
s : Multiset α
⊢ a ∈ s.toList ↔ a ∈ s

Tactic:
rw [← mem_coe, coe_toList]

Result:
no goals
-- Mathlib/Algebra/Free.lean
theorem toFreeSemigroup_comp_map (f : α → β) :
    toFreeSemigroup.comp (map f) = (FreeSemigroup.map f).comp toFreeSemigroup

Proof state:
case h
α : Type u
β : Type v
f : α → β
⊢ ⇑(toFreeSemigroup.comp (map f)) ∘ of = ⇑((FreeSemigroup.map f).comp toFreeSemigroup) ∘ of

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
⊢ toFreeSemigroup.comp (map f) = (FreeSemigroup.map f).comp toFreeSemigroup

Tactic:
ext1

Result:
case h
α : Type u
β : Type v
f : α → β
⊢ ⇑(toFreeSemigroup.comp (map f)) ∘ of = ⇑((FreeSemigroup.map f).comp toFreeSemigroup) ∘ of
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasStrictFDerivAt.smul_const (hc : HasStrictFDerivAt c c' x) (f : F) :
    HasStrictFDerivAt (fun y => c y • f) (c'.smulRight f) x

Proof state:
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : E
𝕜' : Type u_5
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasStrictFDerivAt c c' x
f : F
⊢ HasStrictFDerivAt (fun y => c y • f) (c'.smulRight f) x

Tactic:
simpa only [smul_zero, zero_add] using hc.smul (hasStrictFDerivAt_const f x)

Result:
no goals
-- Mathlib/Data/Nat/BitIndices.lean
theorem bitIndices_one : bitIndices 1 = [0]

Proof state:
⊢ bitIndices 1 = [0]

Tactic:
simp [bitIndices]

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem union_ae_eq_univ_of_ae_eq_univ_right (h : t =ᵐ[μ] univ) : (s ∪ t : Set α) =ᵐ[μ] univ

Proof state:
case h.e'_5
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] univ
⊢ univ = s ∪ univ

Tactic:
rw [union_univ]

Result:
no goals

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] univ
⊢ s ∪ t =ᶠ[ae μ] univ

Tactic:
convert ae_eq_set_union (ae_eq_refl s) h

Result:
case h.e'_5
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
h : t =ᶠ[ae μ] univ
⊢ univ = s ∪ univ
-- Mathlib/Logic/Equiv/Defs.lean
theorem cast_trans {α β γ} (h : α = β) (h2 : β = γ) :
    (Equiv.cast h).trans (Equiv.cast h2) = Equiv.cast (h.trans h2) :=
  ext fun x => by substs h h2; rfl

Proof state:
α β γ : Sort u_1
h : α = β
h2 : β = γ
x : α
⊢ ((Equiv.cast h).trans (Equiv.cast h2)) x = (Equiv.cast ⋯) x

Tactic:
substs h h2

Result:
α : Sort u_1
x : α
⊢ ((Equiv.cast ⋯).trans (Equiv.cast ⋯)) x = (Equiv.cast ⋯) x

Proof state:
α : Sort u_1
x : α
⊢ ((Equiv.cast ⋯).trans (Equiv.cast ⋯)) x = (Equiv.cast ⋯) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_ite_zero (s : Finset ι) (p : ι → Prop) [DecidablePred p]
    (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) (a : M) :
    𝔼 i ∈ s, ite (p i) a 0 = ite (∃ i ∈ s, p i) (a /ℚ #s) 0

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module ℚ≥0 M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
⊢ (𝔼 i ∈ s, if p i then a else 0) = if ∃ i ∈ s, p i then (↑(#s))⁻¹ • a else 0

Tactic:
split_ifs <;> simp [expect, sum_ite_zero _ _ h, *]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem tan_mul_cos {x : ℂ} (hx : cos x ≠ 0) : tan x * cos x = sin x

Proof state:
x : ℂ
hx : cos x ≠ 0
⊢ tan x * cos x = sin x

Tactic:
rw [tan_eq_sin_div_cos, div_mul_cancel₀ _ hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range'_append_1 (s m n : Nat) :
    range' s m ++ range' (s + m) n = range' s (m + n)

Proof state:
s m n : Nat
⊢ range' s m ++ range' (s + m) n = range' s (m + n)

Tactic:
simpa using range'_append s m n 1

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem closure (h : e.IsImage s t) : e.IsImage (closure s) (closure t) := fun x hx => by
  simp only [mem_closure_iff_nhdsWithin_neBot, ← h.map_nhdsWithin_eq hx, map_neBot_iff]

Proof state:
X : Type u_1
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : PartialHomeomorph X Y
s : Set X
t : Set Y
h : e.IsImage s t
x : X
hx : x ∈ e.source
⊢ ↑e x ∈ closure t ↔ x ∈ closure s

Tactic:
simp only [mem_closure_iff_nhdsWithin_neBot, ← h.map_nhdsWithin_eq hx, map_neBot_iff]

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma conductor_eq_zero_iff_level_eq_zero : conductor χ = 0 ↔ n = 0

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ n = 0 → χ.conductor = 0

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R 0
⊢ χ.conductor = 0

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
χ : DirichletCharacter R 0
⊢ χ.conductor = 0

Tactic:
exact Nat.sInf_eq_zero.mpr <| Or.inl <| level_mem_conductorSet χ

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ χ.conductor = 0 ↔ n = 0

Tactic:
refine ⟨(conductor_ne_zero χ).mtr, ?_⟩

Result:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ n = 0 → χ.conductor = 0
-- Mathlib/Topology/UniformSpace/AbstractCompletion.lean
theorem extend_coe [T2Space β] (hf : UniformContinuous f) (a : α) : (pkg.extend f) (ι a) = f a

Proof state:
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : T2Space β
hf : UniformContinuous f
a : α
⊢ pkg.extend f (pkg.coe a) = f a

Tactic:
rw [pkg.extend_def hf]

Result:
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : T2Space β
hf : UniformContinuous f
a : α
⊢ ⋯.extend f (pkg.coe a) = f a

Proof state:
α : Type u_1
inst✝² : UniformSpace α
pkg : AbstractCompletion α
β : Type u_2
inst✝¹ : UniformSpace β
f : α → β
inst✝ : T2Space β
hf : UniformContinuous f
a : α
⊢ ⋯.extend f (pkg.coe a) = f a

Tactic:
exact pkg.isDenseInducing.extend_eq hf.continuous a

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Spectrum.lean
theorem star_eigenvectorUnitary_mulVec (j : n) :
    (star (eigenvectorUnitary hA : Matrix n n 𝕜)) *ᵥ ⇑(hA.eigenvectorBasis j) = Pi.single j 1

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
n : Type u_2
inst✝¹ : Fintype n
A : Matrix n n 𝕜
inst✝ : DecidableEq n
hA : A.IsHermitian
j : n
⊢ star ↑hA.eigenvectorUnitary *ᵥ (WithLp.equiv 2 ((i : n) → (fun x => 𝕜) i)) (hA.eigenvectorBasis j) = Pi.single j 1

Tactic:
rw [← eigenvectorUnitary_mulVec, mulVec_mulVec, unitary.coe_star_mul_self, one_mulVec]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblXYZ_of_Z_eq_zero {P : Fin 3 → R} (hP : W'.Equation P) (hPz : P z = 0) :
    W'.dblXYZ P = P x ^ 2 • ![1, 1, 0]

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ W'.dblXYZ P = P x ^ 2 • ![1, 1, 0]

Tactic:
erw [dblXYZ, dblX_of_Z_eq_zero hP hPz, dblY_of_Z_eq_zero hP hPz, dblZ_of_Z_eq_zero hPz, smul_fin3,
  mul_one, mul_one, mul_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem mem_domain_iff_of_eq_graph {f g : E →ₗ.[R] F} (h : f.graph = g.graph) {x : E} :
    x ∈ f.domain ↔ x ∈ g.domain

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph = g.graph
x : E
⊢ x ∈ f.domain ↔ x ∈ g.domain

Tactic:
simp_rw [mem_domain_iff, h]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
@[simp] lemma length_tail_add_one {p : G.Walk x y} (hp : ¬ p.Nil) :
    p.tail.length + 1 = p.length

Proof state:
V : Type u
G : SimpleGraph V
x y : V
p : G.Walk x y
hp : ¬p.Nil
⊢ p.tail.length + 1 = p.length

Tactic:
rw [← length_cons, cons_tail_eq _ hp]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem of_epi_zero (X Y : C) [Epi (0 : X ⟶ Y)] : IsZero Y :=
  (iff_id_eq_zero Y).mpr ((cancel_epi (0 : X ⟶ Y)).1 (by simp))

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Epi 0
⊢ 0 ≫ 𝟙 Y = 0 ≫ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Sigma.lean
theorem sigma_singleton {a : ∀ i, α i} :
    s.sigma (fun i ↦ ({a i} : Set (α i))) = (fun i ↦ Sigma.mk i <| a i) '' s

Proof state:
ι : Type u_1
α : ι → Type u_3
s : Set ι
a : (i : ι) → α i
⊢ (s.sigma fun i => {a i}) = (fun i => ⟨i, a i⟩) '' s

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
ι : Type u_1
α : ι → Type u_3
s : Set ι
a : (i : ι) → α i
x : ι
y : α x
⊢ (⟨x, y⟩ ∈ s.sigma fun i => {a i}) ↔ ⟨x, y⟩ ∈ (fun i => ⟨i, a i⟩) '' s

Proof state:
case h.mk
ι : Type u_1
α : ι → Type u_3
s : Set ι
a : (i : ι) → α i
x : ι
y : α x
⊢ (⟨x, y⟩ ∈ s.sigma fun i => {a i}) ↔ ⟨x, y⟩ ∈ (fun i => ⟨i, a i⟩) '' s

Tactic:
simp [and_left_comm, eq_comm]

Result:
no goals
-- Mathlib/Data/Bool/Basic.lean
theorem true_eq_false_eq_False : ¬true = false

Proof state:
⊢ ¬true = false

Tactic:
decide

Result:
no goals
-- Mathlib/Topology/Sheaves/Skyscraper.lean
theorem SkyscraperPresheafFunctor.map'_id {a : C} :
    SkyscraperPresheafFunctor.map' p₀ (𝟙 a) = 𝟙 _

Proof state:
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
a : C
⊢ map' p₀ (𝟙 a) = 𝟙 (skyscraperPresheaf p₀ a)

Tactic:
ext U

Result:
case w
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
a : C
U : Opens ↑X
⊢ (map' p₀ (𝟙 a)).app (op U) = (𝟙 (skyscraperPresheaf p₀ a)).app (op U)

Proof state:
case w
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
a : C
U : Opens ↑X
⊢ (map' p₀ (𝟙 a)).app (op U) = (𝟙 (skyscraperPresheaf p₀ a)).app (op U)

Tactic:
simp only [SkyscraperPresheafFunctor.map'_app, NatTrans.id_app]

Result:
case w
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
a : C
U : Opens ↑X
⊢ (if h : p₀ ∈ U then eqToHom ⋯ ≫ 𝟙 a ≫ eqToHom ⋯
    else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj (op U))) =
    (𝟙 (skyscraperPresheaf p₀ a)).app (op U)

Proof state:
case w
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
a : C
U : Opens ↑X
⊢ (if h : p₀ ∈ U then eqToHom ⋯ ≫ 𝟙 a ≫ eqToHom ⋯
    else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj (op U))) =
    (𝟙 (skyscraperPresheaf p₀ a)).app (op U)

Tactic:
split_ifs <;> aesop_cat

Result:
no goals
-- Mathlib/Algebra/Group/Translate.lean
lemma translate_eq_domAddActMk_vadd (a : G) (f : G → α) : τ a f = DomAddAct.mk (-a) +ᵥ f

Proof state:
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a : G
f : G → α
⊢ τ a f = DomAddAct.mk (-a) +ᵥ f

Tactic:
ext

Result:
case h
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a : G
f : G → α
x✝ : G
⊢ τ a f x✝ = (DomAddAct.mk (-a) +ᵥ f) x✝

Proof state:
case h
α : Type u_2
G : Type u_5
inst✝ : AddCommGroup G
a : G
f : G → α
x✝ : G
⊢ τ a f x✝ = (DomAddAct.mk (-a) +ᵥ f) x✝

Tactic:
simp [DomAddAct.vadd_apply, sub_eq_neg_add]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_eq' (r : α → α → Prop) [IsWellOrder α r] (h : IsLimit (type r)) :
    ∃ S : Set α, (∀ a, ∃ b ∈ S, r a b) ∧ #S = cof (type r) :=
  let ⟨S, H, e⟩ := cof_eq r
  ⟨S, fun a =>
    let a' := enum r ⟨_, h.succ_lt (typein_lt_type r a)⟩
    let ⟨b, h, ab⟩ := H a'
    ⟨b, h,
      (IsOrderConnected.conn a b a' <|
            (typein_lt_typein r).1
              (by
                rw [typein_enum]
                exact lt_succ (typein _ _))).resolve_right
        ab⟩,
    e⟩

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
h✝ : (type r).IsLimit
S : Set α
H : Unbounded r S
e : #↑S = (type r).cof
a : α
a' : α := (enum r) ⟨succ ((typein r).toRelEmbedding a), ⋯⟩
b : α
h : b ∈ S
ab : ¬r b a'
⊢ (typein r).toRelEmbedding a < (typein r).toRelEmbedding a'

Tactic:
rw [typein_enum]

Result:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
h✝ : (type r).IsLimit
S : Set α
H : Unbounded r S
e : #↑S = (type r).cof
a : α
a' : α := (enum r) ⟨succ ((typein r).toRelEmbedding a), ⋯⟩
b : α
h : b ∈ S
ab : ¬r b a'
⊢ (typein r).toRelEmbedding a < succ ((typein r).toRelEmbedding a)

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
h✝ : (type r).IsLimit
S : Set α
H : Unbounded r S
e : #↑S = (type r).cof
a : α
a' : α := (enum r) ⟨succ ((typein r).toRelEmbedding a), ⋯⟩
b : α
h : b ∈ S
ab : ¬r b a'
⊢ (typein r).toRelEmbedding a < succ ((typein r).toRelEmbedding a)

Tactic:
exact lt_succ (typein _ _)

Result:
no goals
-- Mathlib/Data/Set/Function.lean
protected lemma RightInvOn.extendDomain (h : RightInvOn g₁ g₂ t) :
    RightInvOn (g₁.extendDomain f) (g₂.extendDomain f) ((↑) ∘ f '' t)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (⇑g₁) (⇑g₂) t
a : α
ha : a ∈ t
⊢ (g₂.extendDomain f) ((g₁.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a

Tactic:
simp_rw [Function.comp_apply, extendDomain_apply_image, h ha]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (⇑g₁) (⇑g₂) t
⊢ RightInvOn (⇑(g₁.extendDomain f)) (⇑(g₂.extendDomain f)) (Subtype.val ∘ ⇑f '' t)

Tactic:
rintro _ ⟨a, ha, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
g₁ g₂ : Perm α
t : Set α
h : RightInvOn (⇑g₁) (⇑g₂) t
a : α
ha : a ∈ t
⊢ (g₂.extendDomain f) ((g₁.extendDomain f) ((Subtype.val ∘ ⇑f) a)) = (Subtype.val ∘ ⇑f) a
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_inter_subset_left [DecidableEq α] :
    image₂ f (s ∩ s') t ⊆ image₂ f s t ∩ image₂ f s' t :=
  coe_subset.1 <| by
    push_cast
    exact image2_inter_subset_left

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst✝ : DecidableEq α
⊢ image2 f (↑s ∩ ↑s') ↑t ⊆ image2 f ↑s ↑t ∩ image2 f ↑s' ↑t

Tactic:
exact image2_inter_subset_left

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst✝ : DecidableEq α
⊢ ↑(image₂ f (s ∩ s') t) ⊆ ↑(image₂ f s t ∩ image₂ f s' t)

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝¹ : DecidableEq γ
f : α → β → γ
s s' : Finset α
t : Finset β
inst✝ : DecidableEq α
⊢ image2 f (↑s ∩ ↑s') ↑t ⊆ image2 f ↑s ↑t ∩ image2 f ↑s' ↑t
-- Mathlib/.lake/packages/lean4/src/lean/Init/ByCases.lean
theorem ite_some_none_eq_none [Decidable P] :
    (if P then some x else none) = none ↔ ¬ P

Proof state:
P : Prop
α✝ : Type u_1
x : α✝
inst✝ : Decidable P
⊢ P → False ↔ ¬P

Tactic:
rfl

Result:
no goals

Proof state:
P : Prop
α✝ : Type u_1
x : α✝
inst✝ : Decidable P
⊢ (if P then some x else none) = none ↔ ¬P

Tactic:
simp only [ite_eq_right_iff, reduceCtorEq]

Result:
P : Prop
α✝ : Type u_1
x : α✝
inst✝ : Decidable P
⊢ P → False ↔ ¬P