harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Asymptotics/Theta.lean
theorem IsTheta.zpow {f : α → 𝕜} {g : α → 𝕜'} (h : f =Θ[l] g) (n : ℤ) :
    (fun x ↦ f x ^ n) =Θ[l] fun x ↦ g x ^ n

Proof state:
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
n : ℤ
⊢ (fun x => f x ^ n) =Θ[l] fun x => g x ^ n

Tactic:
cases n

Result:
case ofNat
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a✝ : ℕ
⊢ (fun x => f x ^ Int.ofNat a✝) =Θ[l] fun x => g x ^ Int.ofNat a✝

case negSucc
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a✝ : ℕ
⊢ (fun x => f x ^ Int.negSucc a✝) =Θ[l] fun x => g x ^ Int.negSucc a✝

Proof state:
case ofNat
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a✝ : ℕ
⊢ (fun x => f x ^ Int.ofNat a✝) =Θ[l] fun x => g x ^ Int.ofNat a✝

Tactic:
simpa only [Int.ofNat_eq_coe, zpow_natCast] using h.pow _

Result:
no goals

Proof state:
case negSucc
α : Type u_1
𝕜 : Type u_14
𝕜' : Type u_15
inst✝¹ : NormedField 𝕜
inst✝ : NormedField 𝕜'
l : Filter α
f : α → 𝕜
g : α → 𝕜'
h : f =Θ[l] g
a✝ : ℕ
⊢ (fun x => f x ^ Int.negSucc a✝) =Θ[l] fun x => g x ^ Int.negSucc a✝

Tactic:
simpa only [zpow_negSucc] using (h.pow _).inv

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem adjointAux_inner_right (A : E →L[𝕜] F) (x : E) (y : F) :
    ⟪x, adjointAux A y⟫ = ⟪A x, y⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace E
A : E →L[𝕜] F
x : E
y : F
⊢ ⟪x, (adjointAux A) y⟫_𝕜 = ⟪A x, y⟫_𝕜

Tactic:
rw [← inner_conj_symm, adjointAux_inner_left, inner_conj_symm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h : len > 0) :
    x.extractLsb' start len = (x.extractLsb (len - 1 + start) start).cast (by omega)

Proof state:
w : Nat
x : BitVec w
start len : Nat
h : len > 0
⊢ extractLsb' start len x = BitVec.cast ⋯ (extractLsb (len - 1 + start) start x)

Tactic:
apply eq_of_toNat_eq

Result:
case a
w : Nat
x : BitVec w
start len : Nat
h : len > 0
⊢ (extractLsb' start len x).toNat = (BitVec.cast ⋯ (extractLsb (len - 1 + start) start x)).toNat

Proof state:
w : Nat
x : BitVec w
start len : Nat
h : len > 0
⊢ len - 1 + 1 = len

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
start len : Nat
h : len > 0
⊢ len - 1 + start - start + 1 = len

Tactic:
omega

Result:
no goals

Proof state:
case a
w : Nat
x : BitVec w
start len : Nat
h : len > 0
⊢ (extractLsb' start len x).toNat = (BitVec.cast ⋯ (extractLsb (len - 1 + start) start x)).toNat

Tactic:
simp [extractLsb, show len - 1 + 1 = len by omega]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasFDerivAt.smul (hc : HasFDerivAt c c' x) (hf : HasFDerivAt f f' x) :
    HasFDerivAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) 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
f : E → F
f' : E →L[𝕜] F
x : E
𝕜' : Type u_5
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : E → 𝕜'
c' : E →L[𝕜] 𝕜'
hc : HasFDerivAt c c' x
hf : HasFDerivAt f f' x
⊢ HasFDerivAt (fun y => c y • f y) (c x • f' + c'.smulRight (f x)) x

Tactic:
exact (isBoundedBilinearMap_smul.hasFDerivAt (𝕜 := 𝕜) (c x, f x) :).comp x <| hc.prod hf

Result:
no goals
-- Mathlib/Control/Applicative.lean
theorem Applicative.pure_seq_eq_map' (f : α → β) : ((pure f : F (α → β)) <*> ·) = (f <$> ·)

Proof state:
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β : Type u
f : α → β
⊢ (fun x => pure f <*> x) = fun x => f <$> x

Tactic:
ext

Result:
case h
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β : Type u
f : α → β
x✝ : F α
⊢ pure f <*> x✝ = f <$> x✝

Proof state:
case h
F : Type u → Type v
inst✝¹ : Applicative F
inst✝ : LawfulApplicative F
α β : Type u
f : α → β
x✝ : F α
⊢ pure f <*> x✝ = f <$> x✝

Tactic:
simp [functor_norm]

Result:
no goals
-- Mathlib/Algebra/Module/Torsion.lean
theorem torsionBySet_isInternal {p : ι → Ideal R}
    (hp : (S : Set ι).Pairwise fun i j => p i ⊔ p j = ⊤)
    (hM : Module.IsTorsionBySet R M (⨅ i ∈ S, p i : Ideal R)) :
    DirectSum.IsInternal fun i : S => torsionBySet R M <| p i :=
  DirectSum.isInternal_submodule_of_iSupIndep_of_iSup_eq_top
    (iSupIndep_iff_supIndep.mpr <| supIndep_torsionBySet_ideal hp)
    (by
      apply (iSup_subtype'' ↑S fun i => torsionBySet R M <| p i).trans
      -- Porting note: times out if we change apply below to <|
      apply (iSup_torsionBySet_ideal_eq_torsionBySet_iInf hp).trans <|
        (Module.isTorsionBySet_iff_torsionBySet_eq_top _).mp hM)

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
p : ι → Ideal R
hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤
hM : Module.IsTorsionBySet R M ↑(⨅ i ∈ S, p i)
⊢ ⨆ i, torsionBySet R M ↑(p ↑i) = ⊤

Tactic:
apply (iSup_subtype'' ↑S fun i => torsionBySet R M <| p i).trans

Result:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
p : ι → Ideal R
hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤
hM : Module.IsTorsionBySet R M ↑(⨅ i ∈ S, p i)
⊢ ⨆ t ∈ ↑S, torsionBySet R M ↑(p t) = ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : DecidableEq ι
S : Finset ι
p : ι → Ideal R
hp : (↑S).Pairwise fun i j => p i ⊔ p j = ⊤
hM : Module.IsTorsionBySet R M ↑(⨅ i ∈ S, p i)
⊢ ⨆ t ∈ ↑S, torsionBySet R M ↑(p t) = ⊤

Tactic:
apply (iSup_torsionBySet_ideal_eq_torsionBySet_iInf hp).trans <|
  (Module.isTorsionBySet_iff_torsionBySet_eq_top _).mp hM

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem diam_smul₀ (c : 𝕜) (x : Set E) : diam (c • x) = ‖c‖ * diam x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
x : Set E
⊢ diam (c • x) = ‖c‖ * diam x

Tactic:
simp_rw [diam, ediam_smul₀, ENNReal.toReal_smul, NNReal.smul_def, coe_nnnorm, smul_eq_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem map_id_fun : map (id : α → α) = id

Proof state:
α : Type u_1
⊢ map id = id

Tactic:
funext l

Result:
case h
α : Type u_1
l : Array α
⊢ map id l = id l

Proof state:
case h
α : Type u_1
l : Array α
⊢ map id l = id l

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem affineSpan_insert_eq_affineSpan {p : P} {ps : Set P} (h : p ∈ affineSpan k ps) :
    affineSpan k (insert p ps) = affineSpan k ps

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
ps : Set P
h : p ∈ affineSpan k ps
⊢ affineSpan k (insert p ps) = affineSpan k ps

Tactic:
rw [← mem_coe] 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
inst✝ : AffineSpace V P
p : P
ps : Set P
h : p ∈ ↑(affineSpan k ps)
⊢ affineSpan k (insert p ps) = affineSpan k ps

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : P
ps : Set P
h : p ∈ ↑(affineSpan k ps)
⊢ affineSpan k (insert p ps) = affineSpan k ps

Tactic:
rw [← affineSpan_insert_affineSpan, Set.insert_eq_of_mem h, affineSpan_coe]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem isComplement'_of_disjoint_and_mul_eq_univ (h1 : Disjoint H K)
    (h2 : ↑H * ↑K = (Set.univ : Set G)) : IsComplement' H K

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h1 : Disjoint H K
h2 : ↑H * ↑K = univ
g : G
⊢ ∃ a, (fun x => ↑x.1 * ↑x.2) a = g

Tactic:
obtain ⟨h, hh, k, hk, hg⟩ := Set.eq_univ_iff_forall.mp h2 g

Result:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h1 : Disjoint H K
h2 : ↑H * ↑K = univ
g h : G
hh : h ∈ ↑H
k : G
hk : k ∈ ↑K
hg : (fun x1 x2 => x1 * x2) h k = g
⊢ ∃ a, (fun x => ↑x.1 * ↑x.2) a = g

Proof state:
case intro.intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h1 : Disjoint H K
h2 : ↑H * ↑K = univ
g h : G
hh : h ∈ ↑H
k : G
hk : k ∈ ↑K
hg : (fun x1 x2 => x1 * x2) h k = g
⊢ ∃ a, (fun x => ↑x.1 * ↑x.2) a = g

Tactic:
exact ⟨(⟨h, hh⟩, ⟨k, hk⟩), hg⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h1 : Disjoint H K
h2 : ↑H * ↑K = univ
⊢ H.IsComplement' K

Tactic:
refine ⟨mul_injective_of_disjoint h1, fun g => ?_⟩

Result:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h1 : Disjoint H K
h2 : ↑H * ↑K = univ
g : G
⊢ ∃ a, (fun x => ↑x.1 * ↑x.2) a = g
-- Mathlib/RingTheory/Jacobson/Artinian.lean
/-- If `A` is a finite type algebra over an artinian ring `R`,
then `A` is finite over `R` if and only if `dim A = 0`. -/
lemma Module.finite_iff_krullDimLE_zero [IsArtinianRing R] :
    Module.Finite R A ↔ Ring.KrullDimLE 0 A

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra.FiniteType R A
inst✝ : IsArtinianRing R
⊢ Module.Finite R A ↔ Ring.KrullDimLE 0 A

Tactic:
have : IsNoetherianRing A := Algebra.FiniteType.isNoetherianRing R A

Result:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra.FiniteType R A
inst✝ : IsArtinianRing R
this : IsNoetherianRing A
⊢ Module.Finite R A ↔ Ring.KrullDimLE 0 A

Proof state:
R : Type u_1
A : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Algebra.FiniteType R A
inst✝ : IsArtinianRing R
this : IsNoetherianRing A
⊢ Module.Finite R A ↔ Ring.KrullDimLE 0 A

Tactic:
rw [finite_iff_isArtinianRing, isArtinianRing_iff_isNoetherianRing_krullDimLE_zero,
  and_iff_right this]

Result:
no goals
-- Mathlib/Logic/Relation.lean
theorem TransGen.swap (h : TransGen r b a) : TransGen (swap r) a b

Proof state:
case single
α : Type u_1
r : α → α → Prop
a b b✝ : α
h : r b b✝
⊢ TransGen (Function.swap r) b✝ b

Tactic:
exact TransGen.single h

Result:
no goals

Proof state:
case tail
α : Type u_1
r : α → α → Prop
a b b✝ c✝ : α
a✝ : TransGen r b b✝
hbc : r b✝ c✝
ih : TransGen (Function.swap r) b✝ b
⊢ TransGen (Function.swap r) c✝ b

Tactic:
exact ih.head hbc

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
a b : α
h : TransGen r b a
⊢ TransGen (Function.swap r) a b

Tactic:
induction h with
| single h => exact TransGen.single h
| tail _ hbc ih => exact ih.head hbc

Result:
no goals
-- Mathlib/GroupTheory/Submonoid/Inverses.lean
theorem leftInvEquiv_symm_mul (x : S) : ((S.leftInvEquiv hS).symm x : M) * x = 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ ↑((S.leftInvEquiv hS).symm x) * ↑x = 1

Tactic:
convert S.mul_leftInvEquiv hS ((S.leftInvEquiv hS).symm x)

Result:
case h.e'_2.h.e'_6.h.e'_3
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ x = (S.leftInvEquiv hS) ((S.leftInvEquiv hS).symm x)

Proof state:
case h.e'_2.h.e'_6.h.e'_3
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S
⊢ x = (S.leftInvEquiv hS) ((S.leftInvEquiv hS).symm x)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Basic.lean
theorem subset_coe_map (f : α →o β) : ∀ s : Interval α, f '' s ⊆ s.map f
  | ⊥ => by simp
  | (s : NonemptyInterval α) => s.subset_coe_map _

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
inst✝ : PartialOrder β
f : α →o β
⊢ ⇑f '' ↑⊥ ⊆ ↑(map f ⊥)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/FinEnum.lean
theorem Finset.mem_enum [DecidableEq α] (s : Finset α) (xs : List α) :
    s ∈ Finset.enum xs ↔ ∀ x ∈ s, x ∈ xs

Proof state:
case cons
α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
⊢ s ∈ enum (x :: xs) ↔ ∀ x_1 ∈ s, x_1 ∈ x :: xs

Tactic:
simp only [enum, List.bind_eq_flatMap, List.mem_flatMap, List.mem_cons, List.mem_singleton,
  List.not_mem_nil, or_false, ih]

Result:
case cons
α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
⊢ (∃ a, (∀ x ∈ a, x ∈ xs) ∧ (s = a ∨ s = insert x a)) ↔ ∀ x_1 ∈ s, x_1 = x ∨ x_1 ∈ xs

Proof state:
case cons
α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
⊢ (∃ a, (∀ x ∈ a, x ∈ xs) ∧ (s = a ∨ s = insert x a)) ↔ ∀ x_1 ∈ s, x_1 = x ∨ x_1 ∈ xs

Tactic:
refine ⟨by aesop, fun hs => ⟨s.erase x, ?_⟩⟩

Result:
case cons
α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
hs : ∀ x_1 ∈ s, x_1 = x ∨ x_1 ∈ xs
⊢ (∀ x_1 ∈ s.erase x, x_1 ∈ xs) ∧ (s = s.erase x ∨ s = insert x (s.erase x))

Proof state:
case cons
α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
hs : ∀ x_1 ∈ s, ¬x_1 = x → x_1 ∈ xs
⊢ (∀ x_1 ∈ s.erase x, x_1 ∈ xs) ∧ (s = s.erase x ∨ s = insert x (s.erase x))

Tactic:
simp +contextual [eq_comm (a := s), or_iff_not_imp_left, hs]

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
⊢ (∃ a, (∀ x ∈ a, x ∈ xs) ∧ (s = a ∨ s = insert x a)) → ∀ x_1 ∈ s, x_1 = x ∨ x_1 ∈ xs

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u
inst✝ : DecidableEq α
s : Finset α
xs : List α
⊢ s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs

Tactic:
induction xs generalizing s with
| nil => simp [enum, eq_empty_iff_forall_not_mem]
| cons x xs ih =>
    simp only [enum, List.bind_eq_flatMap, List.mem_flatMap, List.mem_cons, List.mem_singleton,
      List.not_mem_nil, or_false, ih]
    refine ⟨by aesop, fun hs => ⟨s.erase x, ?_⟩⟩
    simp only [or_iff_not_imp_left] at hs
    simp +contextual [eq_comm (a := s), or_iff_not_imp_left, hs]

Result:
no goals

Proof state:
case cons
α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
hs : ∀ x_1 ∈ s, x_1 = x ∨ x_1 ∈ xs
⊢ (∀ x_1 ∈ s.erase x, x_1 ∈ xs) ∧ (s = s.erase x ∨ s = insert x (s.erase x))

Tactic:
simp only [or_iff_not_imp_left] at hs

Result:
case cons
α : Type u
inst✝ : DecidableEq α
x : α
xs : List α
ih : ∀ (s : Finset α), s ∈ enum xs ↔ ∀ x ∈ s, x ∈ xs
s : Finset α
hs : ∀ x_1 ∈ s, ¬x_1 = x → x_1 ∈ xs
⊢ (∀ x_1 ∈ s.erase x, x_1 ∈ xs) ∧ (s = s.erase x ∨ s = insert x (s.erase x))

Proof state:
case nil
α : Type u
inst✝ : DecidableEq α
s : Finset α
⊢ s ∈ enum [] ↔ ∀ x ∈ s, x ∈ []

Tactic:
simp [enum, eq_empty_iff_forall_not_mem]

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
lemma card_union_eq_card_add_card : #(s ∪ t) = #s + #t ↔ Disjoint s t

Proof state:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(s ∪ t) = #s + #t ↔ Disjoint s t

Tactic:
rw [← card_union_add_card_inter]

Result:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(s ∪ t) = #(s ∪ t) + #(s ∩ t) ↔ Disjoint s t

Proof state:
α : Type u_1
s t : Finset α
inst✝ : DecidableEq α
⊢ #(s ∪ t) = #(s ∪ t) + #(s ∩ t) ↔ Disjoint s t

Tactic:
simp [disjoint_iff_inter_eq_empty]

Result:
no goals
-- Mathlib/CategoryTheory/Idempotents/Karoubi.lean
theorem decompId_i_naturality {P Q : Karoubi C} (f : P ⟶ Q) :
    f ≫ decompId_i Q = decompId_i P ≫ (by exact Hom.mk f.f (by simp))

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ f ≫ Q.decompId_i = P.decompId_i ≫ { f := f.f, comm := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{?u.41876, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ f.f = { X := P.X, p := 𝟙 P.X, idem := ⋯ }.p ≫ f.f ≫ { X := Q.X, p := 𝟙 Q.X, idem := ⋯ }.p

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{?u.41876, u_1} C
P Q : Karoubi C
f : P ⟶ Q
⊢ { X := P.X, p := 𝟙 P.X, idem := ⋯ } ⟶ { X := Q.X, p := 𝟙 Q.X, idem := ⋯ }

Tactic:
exact Hom.mk f.f (by simp)

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
theorem independent_maxGenEigenspace [NoZeroSMulDivisors R M] (f : End R M) :
    iSupIndep f.maxGenEigenspace

Proof state:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : End R M
⊢ iSupIndep f.maxGenEigenspace

Tactic:
apply independent_genEigenspace

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem pow_factors [Nontrivial α] {a : Associates α} {k : ℕ} :
    (a ^ k).factors = k • a.factors

Proof state:
case succ
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a : Associates α
n : ℕ
h : (a ^ n).factors = n • a.factors
⊢ (a ^ (n + 1)).factors = (n + 1) • a.factors

Tactic:
rw [pow_succ, succ_nsmul, factors_mul, h]

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a : Associates α
⊢ (a ^ 0).factors = 0 • a.factors

Tactic:
rw [zero_nsmul, pow_zero]

Result:
case zero
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a : Associates α
⊢ factors 1 = 0

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a : Associates α
k : ℕ
⊢ (a ^ k).factors = k • a.factors

Tactic:
induction' k with n h

Result:
case zero
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a : Associates α
⊢ (a ^ 0).factors = 0 • a.factors

case succ
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a : Associates α
n : ℕ
h : (a ^ n).factors = n • a.factors
⊢ (a ^ (n + 1)).factors = (n + 1) • a.factors

Proof state:
case zero
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a : Associates α
⊢ factors 1 = 0

Tactic:
exact factors_one

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Covering.lean
theorem Prefunctor.symmetrifyCostar (u : U) :
    φ.symmetrify.costar u =
      (Quiver.symmetrifyCostar _).symm ∘
        Sum.map (φ.costar u) (φ.star u) ∘ Quiver.symmetrifyCostar u

Proof state:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
⊢ ⇑(symmetrifyCostar (φ.obj u)) ∘ φ.symmetrify.costar u = Sum.map (φ.costar u) (φ.star u) ∘ ⇑(symmetrifyCostar u)

Tactic:
ext ⟨v, f | g⟩ <;>
  simp only [Quiver.symmetrifyCostar, Function.comp_apply] <;>
  erw [Equiv.sigmaSumDistrib_apply, Equiv.sigmaSumDistrib_apply] <;>
  simp

Result:
no goals

Proof state:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
⊢ φ.symmetrify.costar u = ⇑(symmetrifyCostar (φ.obj u)).symm ∘ Sum.map (φ.costar u) (φ.star u) ∘ ⇑(symmetrifyCostar u)

Tactic:
erw [Equiv.eq_symm_comp]

Result:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
⊢ ⇑(symmetrifyCostar (φ.obj u)) ∘ φ.symmetrify.costar u = Sum.map (φ.costar u) (φ.star u) ∘ ⇑(symmetrifyCostar u)
-- Mathlib/Algebra/Lie/Weights/Killing.lean
lemma IsZero.neg (h : α.IsZero) : (-α).IsZero

Proof state:
K : Type u_2
L : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
h : α.IsZero
⊢ (-α).IsZero

Tactic:
ext

Result:
case h
K : Type u_2
L : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
h : α.IsZero
x✝ : ↥H
⊢ (-α) x✝ = 0 x✝

Proof state:
case h
K : Type u_2
L : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
inst✝² : IsKilling K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
h : α.IsZero
x✝ : ↥H
⊢ (-α) x✝ = 0 x✝

Tactic:
rw [coe_neg, h, neg_zero]

Result:
no goals
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem coe_iInf {ι : Sort*} {S : ι → Subsemiring R} : (↑(⨅ i, S i) : Set R) = ⋂ i, S i

Proof state:
R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
S : ι → Subsemiring R
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
simp only [iInf, coe_sInf, Set.biInter_range]

Result:
no goals
-- Mathlib/Order/Chain.lean
theorem succChain_spec (h : ∃ t, IsChain r s ∧ SuperChain r s t) :
    SuperChain r s (SuccChain r s)

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
h : ∃ t, IsChain r s ∧ SuperChain r s t
this : IsChain r s ∧ SuperChain r s h.choose
⊢ SuperChain r s (SuccChain r s)

Tactic:
simpa [SuccChain, dif_pos, exists_and_left.mp h] using this.2

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
h : ∃ t, IsChain r s ∧ SuperChain r s t
⊢ SuperChain r s (SuccChain r s)

Tactic:
have : IsChain r s ∧ SuperChain r s h.choose := h.choose_spec

Result:
α : Type u_1
r : α → α → Prop
s : Set α
h : ∃ t, IsChain r s ∧ SuperChain r s t
this : IsChain r s ∧ SuperChain r s h.choose
⊢ SuperChain r s (SuccChain r s)
-- Mathlib/Data/Finset/MulAntidiagonal.lean
theorem mem_mulAntidiagonal : x ∈ mulAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a

Proof state:
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
a : α
x : α × α
⊢ x ∈ mulAntidiagonal hs ht a ↔ x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 * x.2 = a

Tactic:
simp only [mulAntidiagonal, Set.Finite.mem_toFinset, Set.mem_mulAntidiagonal]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
private lemma nonsingular_add_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Nonsingular P)
    (hQ : W.Nonsingular Q) (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
    (hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)) : W.Nonsingular
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)), 1] :=
  (nonsingular_some ..).mpr <| Affine.nonsingular_add ((nonsingular_of_Z_ne_zero hPz).mp hP)
    ((nonsingular_of_Z_ne_zero hQz).mp hQ) <| by rwa [← X_eq_iff hPz hQz, ← Y_eq_iff' hPz hQz]

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
⊢ ¬(P x / P z ^ 2 = Q x / Q z ^ 2 ∧ P y / P z ^ 3 = (toAffine W).negY (Q x / Q z ^ 2) (Q y / Q z ^ 3))

Tactic:
rwa [← X_eq_iff hPz hQz, ← Y_eq_iff' hPz hQz]

Result:
no goals