harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Complement.lean
theorem range_mem_leftTransversals {f : G ⧸ H → G} (hf : ∀ q, ↑(f q) = q) :
    Set.range f ∈ leftTransversals (H : Set G) :=
  mem_leftTransversals_iff_bijective.mpr
    ⟨by rintro ⟨-, q₁, rfl⟩ ⟨-, q₂, rfl⟩ h
        exact Subtype.ext <| congr_arg f <| ((hf q₁).symm.trans h).trans (hf q₂),
      fun q => ⟨⟨f q, q, rfl⟩, hf q⟩⟩

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
⊢ Injective ((range f).restrict Quotient.mk'')

Tactic:
rintro ⟨-, q₁, rfl⟩ ⟨-, q₂, rfl⟩ h

Result:
case mk.intro.mk.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
q₁ q₂ : G ⧸ H
h : (range f).restrict Quotient.mk'' ⟨f q₁, ⋯⟩ = (range f).restrict Quotient.mk'' ⟨f q₂, ⋯⟩
⊢ ⟨f q₁, ⋯⟩ = ⟨f q₂, ⋯⟩

Proof state:
case mk.intro.mk.intro
G : Type u_1
inst✝ : Group G
H : Subgroup G
f : G ⧸ H → G
hf : ∀ (q : G ⧸ H), ↑(f q) = q
q₁ q₂ : G ⧸ H
h : (range f).restrict Quotient.mk'' ⟨f q₁, ⋯⟩ = (range f).restrict Quotient.mk'' ⟨f q₂, ⋯⟩
⊢ ⟨f q₁, ⋯⟩ = ⟨f q₂, ⋯⟩

Tactic:
exact Subtype.ext <| congr_arg f <| ((hf q₁).symm.trans h).trans (hf q₂)

Result:
no goals
-- Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean
theorem mem_iff_eq_smul_annIdealGenerator {p : 𝕜[X]} (a : A) :
    p ∈ annIdeal 𝕜 a ↔ ∃ s : 𝕜[X], p = s • annIdealGenerator 𝕜 a

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
p : 𝕜[X]
a : A
⊢ p ∈ annIdeal 𝕜 a ↔ ∃ s, p = s • annIdealGenerator 𝕜 a

Tactic:
simp_rw [@eq_comm _ p, ← mem_span_singleton, ← span_singleton_annIdealGenerator 𝕜 a, Ideal.span]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Monoidal/Normalize.lean
theorem evalWhiskerRight_cons_of_of {f g h i j : C}
    {α : f ≅ g} {η : g ⟶ h} {ηs : h ⟶ i} {ηs₁ : h ⊗ j ⟶ i ⊗ j}
    {η₁ : g ⊗ j ⟶ h ⊗ j} {η₂ : g ⊗ j ⟶ i ⊗ j} {η₃ : f ⊗ j ⟶ i ⊗ j}
    (e_ηs₁ : ηs ▷ j = ηs₁) (e_η₁ : η ▷ j = η₁)
    (e_η₂ : η₁ ≫ ηs₁ = η₂) (e_η₃ : (whiskerRightIso α j).hom ≫ η₂ = η₃) :
    (α.hom ≫ η ≫ ηs) ▷ j = η₃

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
f g h i j : C
α : f ≅ g
η : g ⟶ h
ηs : h ⟶ i
ηs₁ : h ⊗ j ⟶ i ⊗ j
η₁ : g ⊗ j ⟶ h ⊗ j
η₂ : g ⊗ j ⟶ i ⊗ j
η₃ : f ⊗ j ⟶ i ⊗ j
e_ηs₁ : ηs ▷ j = ηs₁
e_η₁ : η ▷ j = η₁
e_η₂ : η₁ ≫ ηs₁ = η₂
e_η₃ : (whiskerRightIso α j).hom ≫ η₂ = η₃
⊢ (α.hom ≫ η ≫ ηs) ▷ j = η₃

Tactic:
simp_all

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prod.triangle [HasBinaryProducts C] (X Y : C) :
    (prod.associator X (⊤_ C) Y).hom ≫ prod.map (𝟙 X) (prod.leftUnitor Y).hom =
      prod.map (prod.rightUnitor X).hom (𝟙 Y)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
X Y : C
⊢ (associator X (⊤_ C) Y).hom ≫ map (𝟙 X) (leftUnitor Y).hom = map (rightUnitor X).hom (𝟙 Y)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean
theorem prodZeroIso_iso_inv_snd (X : C) : (prodZeroIso X).inv ≫ prod.fst = 𝟙 X

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ (prodZeroIso X).inv ≫ prod.fst = 𝟙 X

Tactic:
dsimp [prodZeroIso, binaryFanZeroRight]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ (limit.isoLimitCone { cone := BinaryFan.mk (𝟙 X) 0, isLimit := binaryFanZeroRightIsLimit X }).inv ≫ prod.fst = 𝟙 X

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ (limit.isoLimitCone { cone := BinaryFan.mk (𝟙 X) 0, isLimit := binaryFanZeroRightIsLimit X }).inv ≫ prod.fst = 𝟙 X

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prod.diag_map_fst_snd_comp [HasLimitsOfShape (Discrete WalkingPair) C] {X X' Y Y' : C}
    (g : X ⟶ Y) (g' : X' ⟶ Y') :
    diag (X ⨯ X') ≫ prod.map (prod.fst ≫ g) (prod.snd ≫ g') = prod.map g g'

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasLimitsOfShape (Discrete WalkingPair) C
X X' Y Y' : C
g : X ⟶ Y
g' : X' ⟶ Y'
⊢ diag (X ⨯ X') ≫ map (fst ≫ g) (snd ≫ g') = map g g'

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Bounds/Basic.lean
theorem IsGreatest.union [LinearOrder γ] {a b : γ} {s t : Set γ} (ha : IsGreatest s a)
    (hb : IsGreatest t b) : IsGreatest (s ∪ t) (max a b) :=
  ⟨by rcases le_total a b with h | h <;> simp [h, ha.1, hb.1], (ha.isLUB.union hb.isLUB).1⟩

Proof state:
γ : Type v
inst✝ : LinearOrder γ
a b : γ
s t : Set γ
ha : IsGreatest s a
hb : IsGreatest t b
⊢ a ⊔ b ∈ s ∪ t

Tactic:
rcases le_total a b with h | h <;> simp [h, ha.1, hb.1]

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Properties.lean
theorem apply_dualBasis_right (B : BilinForm K V) (hB : B.Nondegenerate) (sym : B.IsSymm)
    (b : Basis ι K V) (i j) : B (b i) (B.dualBasis hB b j) = if i = j then 1 else 0

Proof state:
V : Type u_5
K : Type u_6
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
ι : Type u_9
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
B : BilinForm K V
hB : B.Nondegenerate
sym : B.IsSymm
b : Basis ι K V
i j : ι
⊢ (B (b i)) ((B.dualBasis hB b) j) = if i = j then 1 else 0

Tactic:
rw [sym.eq, apply_dualBasis_left]

Result:
no goals
-- Mathlib/Algebra/Ring/SumsOfSquares.lean
theorem IsSumSq.sum [AddCommMonoid R] [Mul R] {ι : Type*} {I : Finset ι} {s : ι → R}
    (hs : ∀ i ∈ I, IsSumSq <| s i) : IsSumSq (∑ i ∈ I, s i)

Proof state:
R : Type u_1
inst✝¹ : AddCommMonoid R
inst✝ : Mul R
ι : Type u_2
I : Finset ι
s : ι → R
hs : ∀ i ∈ I, IsSumSq (s i)
⊢ IsSumSq (∑ i ∈ I, s i)

Tactic:
simpa using sum_mem (S := AddSubmonoid.sumSq _) hs

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
theorem χ₄_nat_mod_four (n : ℕ) : χ₄ n = χ₄ (n % 4 : ℕ)

Proof state:
n : ℕ
⊢ χ₄ ↑n = χ₄ ↑(n % 4)

Tactic:
rw [← ZMod.natCast_mod n 4]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem any_append {x y : List α} : (x ++ y).any f = (x.any f || y.any f)

Proof state:
case nil
α : Type u_1
f : α → Bool
y : List α
⊢ ([] ++ y).any f = ([].any f || y.any f)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
f : α → Bool
x y : List α
⊢ (x ++ y).any f = (x.any f || y.any f)

Tactic:
induction x with
| nil => rfl
| cons h t ih => simp_all [Bool.or_assoc]

Result:
no goals

Proof state:
case cons
α : Type u_1
f : α → Bool
y : List α
h : α
t : List α
ih : (t ++ y).any f = (t.any f || y.any f)
⊢ (h :: t ++ y).any f = ((h :: t).any f || y.any f)

Tactic:
simp_all [Bool.or_assoc]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
theorem mapAlgEquiv_trans (e : A₁ ≃ₐ[R] A₂) (f : A₂ ≃ₐ[R] A₃) :
    (mapAlgEquiv σ e).trans (mapAlgEquiv σ f) = mapAlgEquiv σ (e.trans f)

Proof state:
case h.a
R : Type u
σ : Type u_1
inst✝⁶ : CommSemiring R
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
inst✝⁵ : CommSemiring A₁
inst✝⁴ : CommSemiring A₂
inst✝³ : CommSemiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
f : A₂ ≃ₐ[R] A₃
a✝ : MvPolynomial σ A₁
m✝ : σ →₀ ℕ
⊢ coeff m✝ (((mapAlgEquiv σ e).trans (mapAlgEquiv σ f)) a✝) = coeff m✝ ((mapAlgEquiv σ (e.trans f)) a✝)

Tactic:
simp only [AlgEquiv.trans_apply, mapAlgEquiv_apply, map_map]

Result:
case h.a
R : Type u
σ : Type u_1
inst✝⁶ : CommSemiring R
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
inst✝⁵ : CommSemiring A₁
inst✝⁴ : CommSemiring A₂
inst✝³ : CommSemiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
f : A₂ ≃ₐ[R] A₃
a✝ : MvPolynomial σ A₁
m✝ : σ →₀ ℕ
⊢ coeff m✝ ((map ((↑f).comp ↑e)) a✝) = coeff m✝ ((map ↑(e.trans f)) a✝)

Proof state:
case h.a
R : Type u
σ : Type u_1
inst✝⁶ : CommSemiring R
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
inst✝⁵ : CommSemiring A₁
inst✝⁴ : CommSemiring A₂
inst✝³ : CommSemiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
f : A₂ ≃ₐ[R] A₃
a✝ : MvPolynomial σ A₁
m✝ : σ →₀ ℕ
⊢ coeff m✝ ((map ((↑f).comp ↑e)) a✝) = coeff m✝ ((map ↑(e.trans f)) a✝)

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝⁶ : CommSemiring R
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
inst✝⁵ : CommSemiring A₁
inst✝⁴ : CommSemiring A₂
inst✝³ : CommSemiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
f : A₂ ≃ₐ[R] A₃
⊢ (mapAlgEquiv σ e).trans (mapAlgEquiv σ f) = mapAlgEquiv σ (e.trans f)

Tactic:
ext

Result:
case h.a
R : Type u
σ : Type u_1
inst✝⁶ : CommSemiring R
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
inst✝⁵ : CommSemiring A₁
inst✝⁴ : CommSemiring A₂
inst✝³ : CommSemiring A₃
inst✝² : Algebra R A₁
inst✝¹ : Algebra R A₂
inst✝ : Algebra R A₃
e : A₁ ≃ₐ[R] A₂
f : A₂ ≃ₐ[R] A₃
a✝ : MvPolynomial σ A₁
m✝ : σ →₀ ℕ
⊢ coeff m✝ (((mapAlgEquiv σ e).trans (mapAlgEquiv σ f)) a✝) = coeff m✝ ((mapAlgEquiv σ (e.trans f)) a✝)
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean
lemma map_isZero (F : C ⥤ D) [PreservesZeroMorphisms F] {X : C} (hX : IsZero X) :
    IsZero (F.obj X)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
X : C
hX : IsZero X
⊢ IsZero (F.obj X)

Tactic:
simp only [IsZero.iff_id_eq_zero] at hX ⊢

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
X : C
hX : 𝟙 X = 0
⊢ 𝟙 (F.obj X) = 0

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
X : C
hX : 𝟙 X = 0
⊢ 𝟙 (F.obj X) = 0

Tactic:
rw [← F.map_id, hX, F.map_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem add_emod (a b n : Int) : (a + b) % n = (a % n + b % n) % n

Proof state:
a b n : Int
⊢ (a + b) % n = (a % n + b % n) % n

Tactic:
rw [add_emod_emod, emod_add_emod]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[simp]
lemma mem_sum {s : Finset ι} {m : ι → Multiset α} : a ∈ ∑ i ∈ s, m i ↔ ∃ i ∈ s, a ∈ m i

Proof state:
ι : Type u_1
α : Type u_3
a : α
s : Finset ι
m : ι → Multiset α
⊢ a ∈ ∑ i ∈ s, m i ↔ ∃ i ∈ s, a ∈ m i

Tactic:
induction s using Finset.cons_induction <;> simp [*]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem mkMetric_top : (mkMetric (fun _ => ∞ : ℝ≥0∞ → ℝ≥0∞) : Measure X) = ⊤

Proof state:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
⊢ (mkMetric fun x => ⊤).toOuterMeasure = ⊤.toOuterMeasure

Tactic:
rw [mkMetric_toOuterMeasure, OuterMeasure.mkMetric_top, toOuterMeasure_top]

Result:
no goals

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
⊢ (mkMetric fun x => ⊤) = ⊤

Tactic:
apply toOuterMeasure_injective

Result:
case a
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
⊢ (mkMetric fun x => ⊤).toOuterMeasure = ⊤.toOuterMeasure
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_of_getLast? {xs : List α} {a : α} (h : xs.getLast? = some a) : a ∈ xs

Proof state:
case intro
α : Type u_1
a : α
ys : List α
h : (ys ++ [a]).getLast? = some a
⊢ a ∈ ys ++ [a]

Tactic:
exact mem_concat_self ys a

Result:
no goals

Proof state:
α : Type u_1
xs : List α
a : α
h : xs.getLast? = some a
⊢ a ∈ xs

Tactic:
obtain ⟨ys, rfl⟩ := getLast?_eq_some_iff.1 h

Result:
case intro
α : Type u_1
a : α
ys : List α
h : (ys ++ [a]).getLast? = some a
⊢ a ∈ ys ++ [a]
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem subset_support_append_right {V : Type u} {G : SimpleGraph V} {u v w : V}
    (p : G.Walk u v) (q : G.Walk v w) : q.support ⊆ (p.append q).support

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
⊢ q.support ⊆ (p.append q).support

Tactic:
intro h

Result:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : V
⊢ h ∈ q.support → h ∈ (p.append q).support

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : V
⊢ h ∈ q.support → h ∈ (p.append q).support

Tactic:
simp +contextual only [mem_support_append_iff, or_true, imp_true_iff]

Result:
no goals
-- Mathlib/GroupTheory/SchurZassenhaus.lean
theorem eq_one_of_smul_eq_one (hH : Nat.Coprime (Nat.card H) H.index) (α : H.QuotientDiff)
    (h : H) : h • α = α → h = 1 :=
  Quotient.inductionOn' α fun α hα =>
    (powCoprime hH).injective <|
      calc
        h ^ H.index = diff (MonoidHom.id H) (op ((h⁻¹ : H) : G) • α) α

Proof state:
G : Type u_1
inst✝³ : Group G
H : Subgroup G
inst✝² : H.IsCommutative
inst✝¹ : H.FiniteIndex
inst✝ : H.Normal
hH : (Nat.card ↥H).Coprime H.index
α✝ : H.QuotientDiff
h : ↥H
α : H.LeftTransversal
hα : h • Quotient.mk'' α = Quotient.mk'' α
⊢ h ^ H.index = diff (MonoidHom.id ↥H) (op ↑h⁻¹ • α) α

Tactic:
rw [← diff_inv, smul_diff', diff_self, one_mul, inv_pow, inv_inv]

Result:
no goals
-- Mathlib/Data/Multiset/MapFold.lean
theorem map_eq_map {f : α → β} (hf : Function.Injective f) {s t : Multiset α} :
    s.map f = t.map f ↔ s = t

Proof state:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ map f s = map f t ↔ s = t

Tactic:
rw [← rel_eq, ← rel_eq, rel_map]

Result:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ Rel (fun a b => f a = f b) s t ↔ Rel (fun x1 x2 => x1 = x2) s t

Proof state:
α : Type u_1
β : Type v
f : α → β
hf : Injective f
s t : Multiset α
⊢ Rel (fun a b => f a = f b) s t ↔ Rel (fun x1 x2 => x1 = x2) s t

Tactic:
simp only [hf.eq_iff]

Result:
no goals
-- Mathlib/Analysis/SumIntegralComparisons.lean
theorem MonotoneOn.sum_le_integral (hf : MonotoneOn f (Icc x₀ (x₀ + a))) :
    (∑ i ∈ Finset.range a, f (x₀ + i)) ≤ ∫ x in x₀..x₀ + a, f x

Proof state:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∫ (x : ℝ) in x₀..x₀ + ↑a, -f x ≤ ∑ x ∈ Finset.range a, -f (x₀ + ↑x)

Tactic:
exact hf.neg.integral_le_sum

Result:
no goals

Proof state:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∑ i ∈ Finset.range a, f (x₀ + ↑i) ≤ ∫ (x : ℝ) in x₀..x₀ + ↑a, f x

Tactic:
rw [← neg_le_neg_iff, ← Finset.sum_neg_distrib, ← intervalIntegral.integral_neg]

Result:
x₀ : ℝ
a : ℕ
f : ℝ → ℝ
hf : MonotoneOn f (Icc x₀ (x₀ + ↑a))
⊢ ∫ (x : ℝ) in x₀..x₀ + ↑a, -f x ≤ ∑ x ∈ Finset.range a, -f (x₀ + ↑x)
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem nonempty_of_affineSpan_eq_top {s : Set P} (h : affineSpan k s = ⊤) : s.Nonempty

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h : affineSpan k s = ⊤
⊢ s.Nonempty

Tactic:
rw [Set.nonempty_iff_ne_empty]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h : affineSpan k s = ⊤
⊢ s ≠ ∅

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
h : affineSpan k ∅ = ⊤
⊢ False

Tactic:
rw [AffineSubspace.span_empty] at h

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
h : ⊥ = ⊤
⊢ False

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Set P
h : affineSpan k s = ⊤
⊢ s ≠ ∅

Tactic:
rintro rfl

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
h : affineSpan k ∅ = ⊤
⊢ False

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
h : ⊥ = ⊤
⊢ False

Tactic:
exact bot_ne_top k V P h

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_div_mul_comm : a * b / (c * d) = a / c * (b / d)

Proof state:
α : Type u_1
inst✝ : DivisionCommMonoid α
a b c d : α
⊢ a * b / (c * d) = a / c * (b / d)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem diag_inter : (s ∩ t).diag = s.diag ∩ t.diag :=
  ext fun x => by simpa only [mem_diag, mem_inter] using and_and_right

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ x ∈ (s ∩ t).diag ↔ x ∈ s.diag ∩ t.diag

Tactic:
simpa only [mem_diag, mem_inter] using and_and_right

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem pos_finrank_genEigenspace_of_hasEigenvalue [FiniteDimensional K V] {f : End K V}
    {k : ℕ} {μ : K} (hx : f.HasEigenvalue μ) (hk : 0 < k) :
    0 < finrank K (f.genEigenspace μ k) :=
  calc
    0 = finrank K (⊥ : Submodule K V)

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
k : ℕ
μ : K
hx : f.HasEigenvalue μ
hk : 0 < k
⊢ 1 ≤ ↑k

Tactic:
simpa using Nat.succ_le_of_lt hk

Result:
no goals

Proof state:
K : Type v
V : Type w
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
k : ℕ
μ : K
hx : f.HasEigenvalue μ
hk : 0 < k
⊢ 0 = finrank K ↥⊥

Tactic:
rw [finrank_bot]

Result:
no goals
-- Mathlib/Probability/UniformOn.lean
theorem uniformOn_empty_meas : (uniformOn ∅ : Measure Ω) = 0

Proof state:
Ω : Type u_1
inst✝ : MeasurableSpace Ω
⊢ uniformOn ∅ = 0

Tactic:
simp [uniformOn]

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem prod_map_snd : (prod p q).map (snd R M M₂) = q

Proof state:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x : M₂
⊢ x ∈ map (snd R M M₂) (p.prod q) ↔ x ∈ q

Tactic:
simp [(⟨0, zero_mem _⟩ : ∃ x, x ∈ p)]

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
⊢ map (snd R M M₂) (p.prod q) = q

Tactic:
ext x

Result:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
p : Submodule R M
q : Submodule R M₂
x : M₂
⊢ x ∈ map (snd R M M₂) (p.prod q) ↔ x ∈ q
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/AdditionalOperations.lean
theorem WF.map [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {f : (a : α) → β a → δ a} :
    (m.map f).WF

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
h : m.WF
f : (a : α) → β a → δ a
⊢ (Raw.map f m).WF

Tactic:
simpa only [map_eq h] using .wf (Raw₀.map f ⟨m, h.size_buckets_pos⟩).2 (Raw₀.wfImp_map (WF.out h))

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
@[simp] private lemma mu'_apply_self (a : α) : mu' 𝕜 a a = 1

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a : α
⊢ (IncidenceAlgebra.mu' 𝕜) a a = 1

Tactic:
simp [mu'_apply]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem hasStrictDerivAt_cosh (x : ℂ) : HasStrictDerivAt cosh (sinh x) x

Proof state:
case h.e'_9
x : ℂ
⊢ (cexp x - cexp (-x)) * 2⁻¹ = (cexp x + cexp (-id x) * -1) * 2⁻¹

Tactic:
rw [id, mul_neg_one, sub_eq_add_neg]

Result:
no goals

Proof state:
x : ℂ
⊢ HasStrictDerivAt cosh ((cexp x - cexp (-x)) * 2⁻¹) x

Tactic:
convert ((hasStrictDerivAt_exp x).add (hasStrictDerivAt_id x).neg.cexp).mul_const (2 : ℂ)⁻¹
  using 1

Result:
case h.e'_9
x : ℂ
⊢ (cexp x - cexp (-x)) * 2⁻¹ = (cexp x + cexp (-id x) * -1) * 2⁻¹

Proof state:
x : ℂ
⊢ HasStrictDerivAt cosh (sinh x) x

Tactic:
simp only [sinh, div_eq_mul_inv]

Result:
x : ℂ
⊢ HasStrictDerivAt cosh ((cexp x - cexp (-x)) * 2⁻¹) x
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
theorem iteratedDeriv_const_sub (hn : 0 < n) (c : F) :
    iteratedDeriv n (fun z => c - f z) x = iteratedDeriv n (-f) x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
x : 𝕜
f : 𝕜 → F
hn : 0 < n
c : F
⊢ iteratedDeriv n (fun z => c - f z) x = iteratedDeriv n (-f) x

Tactic:
simpa only [← iteratedDerivWithin_univ] using iteratedDerivWithin_const_sub hn c

Result:
no goals
-- Mathlib/Topology/Instances/RatLemmas.lean
theorem not_firstCountableTopology_opc : ¬FirstCountableTopology ℚ∞

Proof state:
⊢ ¬FirstCountableTopology ℚ∞

Tactic:
intro

Result:
a✝ : FirstCountableTopology ℚ∞
⊢ False

Proof state:
a✝ : FirstCountableTopology ℚ∞
⊢ False

Tactic:
exact not_countably_generated_nhds_infty_opc inferInstance

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem update_cons_zero : update (cons x p) 0 z = cons z p

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ cons x p j = cons z p j

Tactic:
rw [← this, cons_succ, cons_succ]

Result:
no goals

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
h : ¬j = 0
⊢ update (cons x p) 0 z j = cons z p j

Tactic:
simp only [h, update_of_ne, Ne, not_false_iff]

Result:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
h : ¬j = 0
⊢ cons x p j = cons z p j

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
h : ¬j = 0
⊢ cons x p j = cons z p j

Tactic:
let j' := pred j h

Result:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
⊢ cons x p j = cons z p j

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
⊢ update (cons x p) 0 z = cons z p

Tactic:
ext j

Result:
case h
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
⊢ update (cons x p) 0 z j = cons z p j

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
⊢ update (cons x p) 0 z j = cons z p j

Tactic:
by_cases h : j = 0

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
h : j = 0
⊢ update (cons x p) 0 z j = cons z p j

case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
h : ¬j = 0
⊢ update (cons x p) 0 z j = cons z p j

Proof state:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
⊢ cons x p j = cons z p j

Tactic:
have : j'.succ = j := succ_pred j h

Result:
case neg
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
h : ¬j = 0
j' : Fin n := j.pred h
this : j'.succ = j
⊢ cons x p j = cons z p j

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
h : j = 0
⊢ update (cons x p) 0 z j = cons z p j

Tactic:
rw [h]

Result:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
h : j = 0
⊢ update (cons x p) 0 z 0 = cons z p 0

Proof state:
case pos
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
z : α 0
j : Fin (n + 1)
h : j = 0
⊢ update (cons x p) 0 z 0 = cons z p 0

Tactic:
simp

Result:
no goals