harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Union.lean
theorem image_biUnion [DecidableEq γ] {f : α → β} {s : Finset α} {t : β → Finset γ} :
    (s.image f).biUnion t = s.biUnion fun a => t (f a) :=
  haveI := Classical.decEq α
  Finset.induction_on s rfl fun a s _ ih => by simp only [image_insert, biUnion_insert, ih]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : DecidableEq β
inst✝ : DecidableEq γ
f : α → β
s✝ : Finset α
t : β → Finset γ
this : DecidableEq α
a : α
s : Finset α
x✝ : a ∉ s
ih : (image f s).biUnion t = s.biUnion fun a => t (f a)
⊢ (image f (insert a s)).biUnion t = (insert a s).biUnion fun a => t (f a)

Tactic:
simp only [image_insert, biUnion_insert, ih]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Hermitian.lean
theorem IsHermitian.inv [Fintype m] [DecidableEq m] {A : Matrix m m α} (hA : A.IsHermitian) :
    A⁻¹.IsHermitian

Proof state:
α : Type u_1
m : Type u_3
inst✝³ : CommRing α
inst✝² : StarRing α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
A : Matrix m m α
hA : A.IsHermitian
⊢ A⁻¹.IsHermitian

Tactic:
simp [IsHermitian, conjTranspose_nonsing_inv, hA.eq]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem card_fintypeIio : Fintype.card (Set.Iio b) = b

Proof state:
n : ℕ
b : Fin n
⊢ Fintype.card ↑(Set.Iio b) = ↑b

Tactic:
rw [Fintype.card_ofFinset, card_Iio]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_one_add' (h : 1 + y ≠ 0) (x : ℝ≥0) : x ^ (1 + y) = x * x ^ y

Proof state:
y : ℝ
h : 1 + y ≠ 0
x : ℝ≥0
⊢ x ^ (1 + y) = x * x ^ y

Tactic:
rw [rpow_add' h, rpow_one]

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem toFinset_filter (s : List α) (p : α → Bool) :
    (s.filter p).toFinset = s.toFinset.filter (p ·)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : List α
p : α → Bool
⊢ (filter p s).toFinset = Finset.filter (fun x => p x = true) s.toFinset

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : List α
p : α → Bool
a✝ : α
⊢ a✝ ∈ (filter p s).toFinset ↔ a✝ ∈ Finset.filter (fun x => p x = true) s.toFinset

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s : List α
p : α → Bool
a✝ : α
⊢ a✝ ∈ (filter p s).toFinset ↔ a✝ ∈ Finset.filter (fun x => p x = true) s.toFinset

Tactic:
simp [List.mem_filter]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
lemma negPart_eq_zero_iff (a : A) (ha : IsSelfAdjoint a

Proof state:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ a⁻ = 0 ↔ 0 ≤ a

Tactic:
rw [← posPart_eq_self, eq_comm (b := a)]

Result:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ a⁻ = 0 ↔ a = a⁺

Proof state:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ a⁻ = 0 ↔ a⁺ - a⁻ = a⁺

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ a⁻ = 0 ↔ a = a⁺

Tactic:
nth_rw 2 [← posPart_sub_negPart a]

Result:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℝ A
inst✝⁷ : SMulCommClass ℝ A A
inst✝⁶ : IsScalarTower ℝ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ a⁻ = 0 ↔ a⁺ - a⁻ = a⁺
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_target' : (f.extend I).target = I '' f.target

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ (f.extend I).target = ↑I '' f.target

Tactic:
rw [extend, PartialEquiv.trans_target'', I.source_eq, univ_inter, I.toPartialEquiv_coe]

Result:
no goals
-- Mathlib/Data/Nat/Totient.lean
theorem totient_super_multiplicative (a b : ℕ) : φ a * φ b ≤ φ (a * b)

Proof state:
case inr
a b : ℕ
d : ℕ := a.gcd b
ha0 : 0 < a
⊢ φ a * φ b ≤ φ (a * b)

Tactic:
have hd0 : 0 < d := Nat.gcd_pos_of_pos_left _ ha0

Result:
case inr
a b : ℕ
d : ℕ := a.gcd b
ha0 : 0 < a
hd0 : 0 < d
⊢ φ a * φ b ≤ φ (a * b)

Proof state:
a b : ℕ
d : ℕ := a.gcd b
ha0 : 0 < a
hd0 : 0 < d
⊢ φ (a * b) * φ (a.gcd b) ≤ φ (a * b) * d

Tactic:
apply mul_le_mul_left' (Nat.totient_le d)

Result:
no goals

Proof state:
case inr
a b : ℕ
d : ℕ := a.gcd b
ha0 : 0 < a
hd0 : 0 < d
⊢ φ a * φ b ≤ φ (a * b)

Tactic:
apply le_of_mul_le_mul_right _ hd0

Result:
a b : ℕ
d : ℕ := a.gcd b
ha0 : 0 < a
hd0 : 0 < d
⊢ φ a * φ b * d ≤ φ (a * b) * d

Proof state:
a b : ℕ
⊢ φ a * φ b ≤ φ (a * b)

Tactic:
let d := a.gcd b

Result:
a b : ℕ
d : ℕ := a.gcd b
⊢ φ a * φ b ≤ φ (a * b)

Proof state:
a b : ℕ
d : ℕ := a.gcd b
⊢ φ a * φ b ≤ φ (a * b)

Tactic:
rcases (zero_le a).eq_or_lt with (rfl | ha0)

Result:
case inl
b : ℕ
d : ℕ := gcd 0 b
⊢ φ 0 * φ b ≤ φ (0 * b)

case inr
a b : ℕ
d : ℕ := a.gcd b
ha0 : 0 < a
⊢ φ a * φ b ≤ φ (a * b)

Proof state:
a b : ℕ
d : ℕ := a.gcd b
ha0 : 0 < a
hd0 : 0 < d
⊢ φ a * φ b * d ≤ φ (a * b) * d

Tactic:
rw [← totient_gcd_mul_totient_mul a b, mul_comm]

Result:
a b : ℕ
d : ℕ := a.gcd b
ha0 : 0 < a
hd0 : 0 < d
⊢ φ (a * b) * φ (a.gcd b) ≤ φ (a * b) * d

Proof state:
case inl
b : ℕ
d : ℕ := gcd 0 b
⊢ φ 0 * φ b ≤ φ (0 * b)

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/Galois/Profinite.lean
theorem restrictNormalHom_continuous (L : IntermediateField k K) [Normal k L] :
    Continuous (AlgEquiv.restrictNormalHom (F := k) (K₁ := K) L)

Proof state:
case h
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set (↥L ≃ₐ[k] ↥L)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
x✝ : FiniteDimensional k ↥(IntermediateField.lift L') :=
  Module.Finite.equiv (IntermediateField.liftAlgEquiv L').toLinearEquiv
⊢ ↑(IntermediateField.lift L').fixingSubgroup ⊆ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N ∧
    IsOpen ↑(IntermediateField.lift L').fixingSubgroup ∧ 1 ∈ ↑(IntermediateField.lift L').fixingSubgroup

Tactic:
constructor

Result:
case h.left
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set (↥L ≃ₐ[k] ↥L)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
x✝ : FiniteDimensional k ↥(IntermediateField.lift L') :=
  Module.Finite.equiv (IntermediateField.liftAlgEquiv L').toLinearEquiv
⊢ ↑(IntermediateField.lift L').fixingSubgroup ⊆ ⇑(AlgEquiv.restrictNormalHom ↥L) ⁻¹' N

case h.right
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
L : IntermediateField k K
inst✝ : Normal k ↥L
N : Set (↥L ≃ₐ[k] ↥L)
L' : IntermediateField k ↥L
left✝ : FiniteDimensional k ↥L'
hO : ↑L'.fixingSubgroup ⊆ N
x✝ : FiniteDimensional k ↥(IntermediateField.lift L') :=
  Module.Finite.equiv (IntermediateField.liftAlgEquiv L').toLinearEquiv
⊢ IsOpen ↑(IntermediateField.lift L').fixingSubgroup ∧ 1 ∈ ↑(IntermediateField.lift L').fixingSubgroup
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem mem_zipIdx' {x : α} {i : Nat} {xs : Array α} (h : (x, i) ∈ xs.zipIdx) :
    i < xs.size ∧ x = xs[i]'(by have := le_snd_of_mem_zipIdx h; have := snd_lt_add_of_mem_zipIdx h; omega) :=
  ⟨by simpa using snd_lt_add_of_mem_zipIdx h, fst_eq_of_mem_zipIdx h⟩

Proof state:
α : Type ?u.29452
x : α
i : Nat
xs : Array α
h : (x, i) ∈ xs.zipIdx
this✝ : 0 ≤ (x, i).snd
this : (x, i).snd < 0 + xs.size
⊢ i < xs.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.29452
x : α
i : Nat
xs : Array α
h : (x, i) ∈ xs.zipIdx
this : 0 ≤ (x, i).snd
⊢ i < xs.size

Tactic:
have := snd_lt_add_of_mem_zipIdx h

Result:
α : Type ?u.29452
x : α
i : Nat
xs : Array α
h : (x, i) ∈ xs.zipIdx
this✝ : 0 ≤ (x, i).snd
this : (x, i).snd < 0 + xs.size
⊢ i < xs.size

Proof state:
α : Type ?u.29452
x : α
i : Nat
xs : Array α
h : (x, i) ∈ xs.zipIdx
⊢ i < xs.size

Tactic:
have := le_snd_of_mem_zipIdx h

Result:
α : Type ?u.29452
x : α
i : Nat
xs : Array α
h : (x, i) ∈ xs.zipIdx
this : 0 ≤ (x, i).snd
⊢ i < xs.size

Proof state:
α : Type u_1
x : α
i : Nat
xs : Array α
h : (x, i) ∈ xs.zipIdx
⊢ i < xs.size

Tactic:
simpa using snd_lt_add_of_mem_zipIdx h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/BasicAux.lean
theorem List.toArray_eq_toArray_eq (as bs : List α) : (as.toArray = bs.toArray) = (as = bs)

Proof state:
α : Type u_1
as bs : List α
⊢ (as.toArray = bs.toArray) = (as = bs)

Tactic:
simp

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
theorem εToSingle₀_comp_eq :
    ((forget₂ _ (ModuleCat.{u} k)).mapHomologicalComplex _).map (εToSingle₀ k G) ≫
        (HomologicalComplex.singleMapHomologicalComplex _ _ _).hom.app _ =
      (forget₂ToModuleCatHomotopyEquiv k G).hom

Proof state:
case hfg
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ (forget₂ (Rep k G) (ModuleCat k)).map ((εToSingle₀ k G).f 0) ≫
      ((HomologicalComplex.singleMapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ)
                  0).hom.app
            (Rep.trivial k G k)).f
        0 =
    (forget₂ToModuleCatHomotopyEquiv k G).hom.f 0

Tactic:
simpa using (forget₂ToModuleCatHomotopyEquiv_f_0_eq k G).symm

Result:
no goals

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ ((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G) ≫
      (HomologicalComplex.singleMapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ) 0).hom.app
        (Rep.trivial k G k) =
    (forget₂ToModuleCatHomotopyEquiv k G).hom

Tactic:
ext1

Result:
case hfg
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G) ≫
          (HomologicalComplex.singleMapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ)
                  0).hom.app
            (Rep.trivial k G k)).f
      0 =
    (forget₂ToModuleCatHomotopyEquiv k G).hom.f 0

Proof state:
case hfg
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ (((forget₂ (Rep k G) (ModuleCat k)).mapHomologicalComplex (ComplexShape.down ℕ)).map (εToSingle₀ k G) ≫
          (HomologicalComplex.singleMapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ)
                  0).hom.app
            (Rep.trivial k G k)).f
      0 =
    (forget₂ToModuleCatHomotopyEquiv k G).hom.f 0

Tactic:
dsimp

Result:
case hfg
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ (forget₂ (Rep k G) (ModuleCat k)).map ((εToSingle₀ k G).f 0) ≫
      ((HomologicalComplex.singleMapHomologicalComplex (forget₂ (Rep k G) (ModuleCat k)) (ComplexShape.down ℕ)
                  0).hom.app
            (Rep.trivial k G k)).f
        0 =
    (forget₂ToModuleCatHomotopyEquiv k G).hom.f 0
-- Mathlib/FieldTheory/Separable.lean
theorem separable_X_sub_C {x : R} : Separable (X - C x)

Proof state:
R : Type u
inst✝ : CommRing R
x : R
⊢ (X - C x).Separable

Tactic:
simpa only [sub_eq_add_neg, C_neg] using separable_X_add_C (-x)

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Maximal/Topology.lean
theorem toPrimeSpectrum_range :
    Set.range (@toPrimeSpectrum R _) = { x | IsClosed ({x} : Set <| PrimeSpectrum R) }

Proof state:
R : Type u
inst✝ : CommRing R
⊢ range toPrimeSpectrum = {x | IsClosed {x}}

Tactic:
simp only [isClosed_singleton_iff_isMaximal]

Result:
R : Type u
inst✝ : CommRing R
⊢ range toPrimeSpectrum = {x | x.asIdeal.IsMaximal}

Proof state:
R : Type u
inst✝ : CommRing R
⊢ range toPrimeSpectrum = {x | x.asIdeal.IsMaximal}

Tactic:
ext ⟨x, _⟩

Result:
case h.mk
R : Type u
inst✝ : CommRing R
x : Ideal R
isPrime✝ : x.IsPrime
⊢ { asIdeal := x, isPrime := isPrime✝ } ∈ range toPrimeSpectrum ↔
    { asIdeal := x, isPrime := isPrime✝ } ∈ {x | x.asIdeal.IsMaximal}

Proof state:
case h.mk
R : Type u
inst✝ : CommRing R
x : Ideal R
isPrime✝ : x.IsPrime
⊢ { asIdeal := x, isPrime := isPrime✝ } ∈ range toPrimeSpectrum ↔
    { asIdeal := x, isPrime := isPrime✝ } ∈ {x | x.asIdeal.IsMaximal}

Tactic:
exact ⟨fun ⟨y, hy⟩ => hy ▸ y.isMaximal, fun hx => ⟨⟨x, hx⟩, rfl⟩⟩

Result:
no goals
-- Mathlib/Algebra/FreeAlgebra.lean
theorem liftAux_eq (f : X → A) : liftAux R f = lift R f

Proof state:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ FreeAlgebra.liftAux R f =
    { toFun := FreeAlgebra.liftAux R, invFun := fun F => ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ } f

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ FreeAlgebra.liftAux R f = (lift R) f

Tactic:
rw [lift]

Result:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
⊢ FreeAlgebra.liftAux R f =
    { toFun := FreeAlgebra.liftAux R, invFun := fun F => ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ } f
-- Mathlib/SetTheory/Game/PGame.lean
theorem zero_lf_le {x : PGame} : 0 ⧏ x ↔ ∃ i, 0 ≤ x.moveLeft i

Proof state:
x : PGame
⊢ ((∃ i, 0 ≤ x.moveLeft i) ∨ ∃ j, moveRight 0 j ≤ x) ↔ ∃ i, 0 ≤ x.moveLeft i

Tactic:
simp

Result:
no goals

Proof state:
x : PGame
⊢ 0 ⧏ x ↔ ∃ i, 0 ≤ x.moveLeft i

Tactic:
rw [lf_iff_exists_le]

Result:
x : PGame
⊢ ((∃ i, 0 ≤ x.moveLeft i) ∨ ∃ j, moveRight 0 j ≤ x) ↔ ∃ i, 0 ≤ x.moveLeft i
-- Mathlib/Algebra/Module/Lattice.lean
/-- A finitely-generated `R`-submodule of `V` of rank at least the `K`-rank of `V`
is a lattice. -/
lemma of_rank_le [Module.Finite K V] [IsFractionRing R K] {M : Submodule R V}
    (hfg : M.FG) (hr : Module.rank K V ≤ Module.rank R M) : IsLattice K M where
  fg := hfg
  span_eq_top

Proof state:
R : Type u_1
inst✝⁹ : CommRing R
K : Type u_2
inst✝⁸ : Field K
inst✝⁷ : Algebra R K
V : Type u_3
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module K V
inst✝⁴ : Module R V
inst✝³ : IsScalarTower R K V
inst✝² : IsDomain R
inst✝¹ : Module.Finite K V
inst✝ : IsFractionRing R K
M : Submodule R V
hfg : M.FG
hr : Module.rank K V ≤ Module.rank R ↥M
⊢ span K ↑M = ⊤

Tactic:
simpa using Submodule.span_range_eq_top_of_injective_of_rank_le M.injective_subtype hr

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem bihimp_eq_bot : a ⇔ b = ⊥ ↔ IsCompl a b

Proof state:
α : Type u_2
inst✝ : BooleanAlgebra α
a b : α
⊢ a ⇔ b = ⊥ ↔ IsCompl a b

Tactic:
rw [bihimp_eq', ← compl_sup, sup_eq_bot_iff, compl_eq_bot, isCompl_iff, disjoint_iff,
  codisjoint_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem coordinate_eval (i : Nat) (v : Coeffs) :
    (coordinate i).eval v = v.get i

Proof state:
i : Nat
v : Coeffs
⊢ (coordinate i).eval v = v.get i

Tactic:
simp [eval, coordinate]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ushiftRight_eq_zero {x : BitVec w} {n : Nat} (hn : w ≤ n) :
    x >>> n = 0#w

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : w ≤ n
this : 2 ^ w ≤ 2 ^ n
⊢ x.toNat < 2 ^ n

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : w ≤ n
⊢ x >>> n = 0#w

Tactic:
simp only [toNat_eq, toNat_ushiftRight, toNat_ofNat, Nat.zero_mod]

Result:
w : Nat
x : BitVec w
n : Nat
hn : w ≤ n
⊢ x.toNat >>> n = 0

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : w ≤ n
this : 2 ^ w ≤ 2 ^ n
⊢ x.toNat >>> n = 0

Tactic:
rw [Nat.shiftRight_eq_div_pow, Nat.div_eq_of_lt (by omega)]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
n : Nat
hn : w ≤ n
⊢ x.toNat >>> n = 0

Tactic:
have : 2^w ≤ 2^n := Nat.pow_le_pow_of_le Nat.one_lt_two hn

Result:
w : Nat
x : BitVec w
n : Nat
hn : w ≤ n
this : 2 ^ w ≤ 2 ^ n
⊢ x.toNat >>> n = 0
-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean
theorem neg_one_le_mulExpNegMulSq_one (x : ℝ) : -1 ≤ mulExpNegMulSq 1 x

Proof state:
x : ℝ
⊢ -1 ≤ mulExpNegMulSq 1 x

Tactic:
rw [← neg_mulExpNegMulSq_neg, neg_le_neg_iff]

Result:
x : ℝ
⊢ mulExpNegMulSq 1 (-x) ≤ 1

Proof state:
x : ℝ
⊢ mulExpNegMulSq 1 (-x) ≤ 1

Tactic:
exact mulExpNegMulSq_one_le_one (-x)

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toReal_add (ha : a ≠ ∞) (hb : b ≠ ∞) : (a + b).toReal = a.toReal + b.toReal

Proof state:
case intro.intro
a b : ℝ≥0
⊢ (↑a + ↑b).toReal = (↑a).toReal + (↑b).toReal

Tactic:
rfl

Result:
no goals

Proof state:
case intro
b : ℝ≥0∞
hb : b ≠ ⊤
a : ℝ≥0
⊢ (↑a + b).toReal = (↑a).toReal + b.toReal

Tactic:
lift b to ℝ≥0 using hb

Result:
case intro.intro
a b : ℝ≥0
⊢ (↑a + ↑b).toReal = (↑a).toReal + (↑b).toReal

Proof state:
a b : ℝ≥0∞
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ (a + b).toReal = a.toReal + b.toReal

Tactic:
lift a to ℝ≥0 using ha

Result:
case intro
b : ℝ≥0∞
hb : b ≠ ⊤
a : ℝ≥0
⊢ (↑a + b).toReal = (↑a).toReal + b.toReal
-- Mathlib/Topology/Bases.lean
theorem isTopologicalBasis_of_subbasis_of_finiteInter {s : Set (Set α)} (hsg : t = generateFrom s)
    (hsi : FiniteInter s) : IsTopologicalBasis s

Proof state:
case h.e'_3
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
⊢ s = (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}

Tactic:
refine le_antisymm (fun t ht ↦ ⟨{t}, by simpa using ht⟩) ?_

Result:
case h.e'_3
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
⊢ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s} ≤ s

Proof state:
case h.e'_3.intro.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
g : Set (Set α)
hg : g.Finite
hgs : g ⊆ s
⊢ (fun f => ⋂₀ f) g ∈ s

Tactic:
lift g to Finset (Set α) using hg

Result:
case h.e'_3.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
g : Finset (Set α)
hgs : ↑g ⊆ s
⊢ (fun f => ⋂₀ f) ↑g ∈ s

Proof state:
α : Type u
t✝ : TopologicalSpace α
s : Set (Set α)
hsg : t✝ = generateFrom s
hsi : FiniteInter s
t : Set α
ht : t ∈ s
⊢ {t} ∈ {f | f.Finite ∧ f ⊆ s} ∧ (fun f => ⋂₀ f) {t} = t

Tactic:
simpa using ht

Result:
no goals

Proof state:
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
⊢ IsTopologicalBasis s

Tactic:
convert isTopologicalBasis_of_subbasis hsg

Result:
case h.e'_3
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
⊢ s = (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}

Proof state:
case h.e'_3
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
⊢ (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s} ≤ s

Tactic:
rintro _ ⟨g, ⟨hg, hgs⟩, rfl⟩

Result:
case h.e'_3.intro.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
g : Set (Set α)
hg : g.Finite
hgs : g ⊆ s
⊢ (fun f => ⋂₀ f) g ∈ s

Proof state:
case h.e'_3.intro.intro.intro.intro
α : Type u
t : TopologicalSpace α
s : Set (Set α)
hsg : t = generateFrom s
hsi : FiniteInter s
g : Finset (Set α)
hgs : ↑g ⊆ s
⊢ (fun f => ⋂₀ f) ↑g ∈ s

Tactic:
exact hsi.finiteInter_mem g hgs

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_coe_eq_coe_finsetCard (s : Finset α) :
    encard (s : Set α) = s.card

Proof state:
α : Type u_1
s : Finset α
⊢ ↑⋯.toFinset.card = ↑s.card

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
⊢ (↑s).encard = ↑s.card

Tactic:
rw [Finite.encard_eq_coe_toFinset_card (Finset.finite_toSet s)]

Result:
α : Type u_1
s : Finset α
⊢ ↑⋯.toFinset.card = ↑s.card
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Basic.lean
theorem mem_of (h : (v, p) ∈ c) : Mem v c

Proof state:
case true
α✝ : Type u_1
c : Clause α✝
v : α✝
h : (v, true) ∈ c
⊢ Mem v c

Tactic:
right

Result:
case true.h
α✝ : Type u_1
c : Clause α✝
v : α✝
h : (v, true) ∈ c
⊢ (v, true) ∈ c

Proof state:
α✝ : Type u_1
c : Clause α✝
v : α✝
p : Bool
h : (v, p) ∈ c
⊢ Mem v c

Tactic:
cases p

Result:
case false
α✝ : Type u_1
c : Clause α✝
v : α✝
h : (v, false) ∈ c
⊢ Mem v c

case true
α✝ : Type u_1
c : Clause α✝
v : α✝
h : (v, true) ∈ c
⊢ Mem v c

Proof state:
case false.h
α✝ : Type u_1
c : Clause α✝
v : α✝
h : (v, false) ∈ c
⊢ (v, false) ∈ c

Tactic:
exact h

Result:
no goals

Proof state:
case true.h
α✝ : Type u_1
c : Clause α✝
v : α✝
h : (v, true) ∈ c
⊢ (v, true) ∈ c

Tactic:
exact h

Result:
no goals

Proof state:
case false
α✝ : Type u_1
c : Clause α✝
v : α✝
h : (v, false) ∈ c
⊢ Mem v c

Tactic:
left

Result:
case false.h
α✝ : Type u_1
c : Clause α✝
v : α✝
h : (v, false) ∈ c
⊢ (v, false) ∈ c
-- Mathlib/Data/ENNReal/Inv.lean
theorem toNNReal_inv (a : ℝ≥0∞) : a⁻¹.toNNReal = a.toNNReal⁻¹

Proof state:
case coe.inl

⊢ (↑0)⁻¹.toNNReal = (↑0).toNNReal⁻¹

Tactic:
simp

Result:
no goals

Proof state:
case coe.inr
a : ℝ≥0
ha : a ≠ 0
⊢ (↑a)⁻¹.toNNReal = (↑a).toNNReal⁻¹

Tactic:
rw [← coe_inv ha, toNNReal_coe, toNNReal_coe]

Result:
no goals

Proof state:
case top

⊢ ⊤⁻¹.toNNReal = ⊤.toNNReal⁻¹

Tactic:
simp

Result:
no goals

Proof state:
a : ℝ≥0∞
⊢ a⁻¹.toNNReal = a.toNNReal⁻¹

Tactic:
induction' a with a

Result:
case top

⊢ ⊤⁻¹.toNNReal = ⊤.toNNReal⁻¹

case coe
a : ℝ≥0
⊢ (↑a)⁻¹.toNNReal = (↑a).toNNReal⁻¹

Proof state:
case coe
a : ℝ≥0
⊢ (↑a)⁻¹.toNNReal = (↑a).toNNReal⁻¹

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Result:
case coe.inl

⊢ (↑0)⁻¹.toNNReal = (↑0).toNNReal⁻¹

case coe.inr
a : ℝ≥0
ha : a ≠ 0
⊢ (↑a)⁻¹.toNNReal = (↑a).toNNReal⁻¹
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem exp_log_of_neg (hx : x < 0) : exp (log x) = -x

Proof state:
x : ℝ
hx : x < 0
⊢ rexp (log x) = -x

Tactic:
rw [exp_log_eq_abs (ne_of_lt hx)]

Result:
x : ℝ
hx : x < 0
⊢ |x| = -x

Proof state:
x : ℝ
hx : x < 0
⊢ |x| = -x

Tactic:
exact abs_of_neg hx

Result:
no goals
-- Mathlib/Data/Finsupp/ToDFinsupp.lean
theorem sigmaFinsuppEquivDFinsupp_support [DecidableEq ι] [Zero N]
    [∀ (i : ι) (x : η i →₀ N), Decidable (x ≠ 0)] (f : (Σi, η i) →₀ N) :
    (sigmaFinsuppEquivDFinsupp f).support = Finsupp.splitSupport f

Proof state:
case h
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Zero N
inst✝ : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
a✝ : ι
⊢ a✝ ∈ (sigmaFinsuppEquivDFinsupp f).support ↔ a✝ ∈ f.splitSupport

Tactic:
rw [DFinsupp.mem_support_toFun]

Result:
case h
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Zero N
inst✝ : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
a✝ : ι
⊢ (sigmaFinsuppEquivDFinsupp f) a✝ ≠ 0 ↔ a✝ ∈ f.splitSupport

Proof state:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Zero N
inst✝ : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
⊢ (sigmaFinsuppEquivDFinsupp f).support = f.splitSupport

Tactic:
ext

Result:
case h
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Zero N
inst✝ : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
a✝ : ι
⊢ a✝ ∈ (sigmaFinsuppEquivDFinsupp f).support ↔ a✝ ∈ f.splitSupport

Proof state:
case h
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Zero N
inst✝ : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
a✝ : ι
⊢ (sigmaFinsuppEquivDFinsupp f) a✝ ≠ 0 ↔ a✝ ∈ f.splitSupport

Tactic:
exact (Finsupp.mem_splitSupport_iff_nonzero _ _).symm

Result:
no goals