harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem gcd_mul_right {a : α} : (s.gcd fun x ↦ f x * a) = s.gcd f * normalize a

Proof state:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ ∀ ⦃a_1 : β⦄ {s : Finset β},
    a_1 ∉ s →
      (s.gcd fun x => f x * a) = s.gcd f * normalize a →
        ((insert a_1 s).gcd fun x => f x * a) = (insert a_1 s).gcd f * normalize a

Tactic:
intro b t _ h

Result:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : b ∉ t
h : (t.gcd fun x => f x * a) = t.gcd f * normalize a
⊢ ((insert b t).gcd fun x => f x * a) = (insert b t).gcd f * normalize a

Proof state:
case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∅.gcd fun x => f x * a) = ∅.gcd f * normalize a

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : b ∉ t
h : (t.gcd fun x => f x * a) = t.gcd f * normalize a
⊢ ((insert b t).gcd fun x => f x * a) = (insert b t).gcd f * normalize a

Tactic:
rw [gcd_insert, gcd_insert, h, ← gcd_mul_right]

Result:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : b ∉ t
h : (t.gcd fun x => f x * a) = t.gcd f * normalize a
⊢ GCDMonoid.gcd (f b * a) (t.gcd f * normalize a) = GCDMonoid.gcd (f b * a) (t.gcd f * a)

Proof state:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : b ∉ t
h : (t.gcd fun x => f x * a) = t.gcd f * normalize a
⊢ GCDMonoid.gcd (f b * a) (t.gcd f * normalize a) = GCDMonoid.gcd (f b * a) (t.gcd f * a)

Tactic:
apply ((normalize_associated a).mul_left _).gcd_eq_right

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (s.gcd fun x => f x * a) = s.gcd f * normalize a

Tactic:
refine s.induction_on ?_ ?_

Result:
case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∅.gcd fun x => f x * a) = ∅.gcd f * normalize a

case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ ∀ ⦃a_1 : β⦄ {s : Finset β},
    a_1 ∉ s →
      (s.gcd fun x => f x * a) = s.gcd f * normalize a →
        ((insert a_1 s).gcd fun x => f x * a) = (insert a_1 s).gcd f * normalize a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Monadic.lean
theorem foldrM_map [Monad m] [LawfulMonad m] (f : β₁ → β₂) (g : β₂ → α → m α) (l : Array β₁)
    (init : α) (w : start = l.size) :
    (l.map f).foldrM g init start 0 = l.foldrM (fun x y => g (f x) y) init start 0

Proof state:
m : Type u_1 → Type u_2
β₁ : Type u_3
β₂ : Type u_4
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β₁ → β₂
g : β₂ → α → m α
l : Array β₁
init : α
⊢ foldrM g init (map f l) l.size = foldrM (fun x y => g (f x) y) init l

Tactic:
cases l

Result:
case mk
m : Type u_1 → Type u_2
β₁ : Type u_3
β₂ : Type u_4
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β₁ → β₂
g : β₂ → α → m α
init : α
toList✝ : List β₁
⊢ foldrM g init (map f { toList := toList✝ }) { toList := toList✝ }.size =
    foldrM (fun x y => g (f x) y) init { toList := toList✝ }

Proof state:
case mk
m : Type u_1 → Type u_2
β₁ : Type u_3
β₂ : Type u_4
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β₁ → β₂
g : β₂ → α → m α
init : α
toList✝ : List β₁
⊢ foldrM g init (map f { toList := toList✝ }) { toList := toList✝ }.size =
    foldrM (fun x y => g (f x) y) init { toList := toList✝ }

Tactic:
simp [List.foldrM_map]

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
β₁ : Type u_3
β₂ : Type u_4
α : Type u_1
start : Nat
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β₁ → β₂
g : β₂ → α → m α
l : Array β₁
init : α
w : start = l.size
⊢ foldrM g init (map f l) start = foldrM (fun x y => g (f x) y) init l start

Tactic:
subst w

Result:
m : Type u_1 → Type u_2
β₁ : Type u_3
β₂ : Type u_4
α : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : β₁ → β₂
g : β₂ → α → m α
l : Array β₁
init : α
⊢ foldrM g init (map f l) l.size = foldrM (fun x y => g (f x) y) init l
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem contains_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} :
    (m.alter k f).contains k = (f (m.get? k)).isSome

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
⊢ (m.alter k f).contains k = (f (m.get? k)).isSome

Tactic:
simp only [contains_alter, beq_self_eq_true, reduceIte]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivWithinAt.smul (hc : HasDerivWithinAt c c' s x) (hf : HasDerivWithinAt f f' s x) :
    HasDerivWithinAt (fun y => c y • f y) (c x • f' + c' • f x) s x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' s x
hf : HasDerivWithinAt f f' s x
⊢ HasDerivWithinAt (fun y => c y • f y) (c x • f' + c' • f x) s x

Tactic:
simpa using (HasFDerivWithinAt.smul hc hf).hasDerivWithinAt

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem range_dualMap_le_dualAnnihilator_ker :
    LinearMap.range f.dualMap ≤ f.ker.dualAnnihilator

Proof state:
case intro
R : Type uR
inst✝⁴ : CommSemiring R
M₁ : Type uM₁
M₂ : Type uM₂
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
ψ : Dual R M₂
x : M₁
hx : f x = 0
⊢ (f.dualMap ψ) x = 0

Tactic:
rw [dualMap_apply, hx, map_zero]

Result:
no goals

Proof state:
case intro
R : Type uR
inst✝⁴ : CommSemiring R
M₁ : Type uM₁
M₂ : Type uM₂
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
ψ : Dual R M₂
⊢ f.dualMap ψ ∈ (ker f).dualAnnihilator

Tactic:
simp_rw [Submodule.mem_dualAnnihilator, mem_ker]

Result:
case intro
R : Type uR
inst✝⁴ : CommSemiring R
M₁ : Type uM₁
M₂ : Type uM₂
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
ψ : Dual R M₂
⊢ ∀ (w : M₁), f w = 0 → (f.dualMap ψ) w = 0

Proof state:
case intro
R : Type uR
inst✝⁴ : CommSemiring R
M₁ : Type uM₁
M₂ : Type uM₂
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
ψ : Dual R M₂
⊢ ∀ (w : M₁), f w = 0 → (f.dualMap ψ) w = 0

Tactic:
rintro x hx

Result:
case intro
R : Type uR
inst✝⁴ : CommSemiring R
M₁ : Type uM₁
M₂ : Type uM₂
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
ψ : Dual R M₂
x : M₁
hx : f x = 0
⊢ (f.dualMap ψ) x = 0

Proof state:
R : Type uR
inst✝⁴ : CommSemiring R
M₁ : Type uM₁
M₂ : Type uM₂
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
⊢ range f.dualMap ≤ (ker f).dualAnnihilator

Tactic:
rintro _ ⟨ψ, rfl⟩

Result:
case intro
R : Type uR
inst✝⁴ : CommSemiring R
M₁ : Type uM₁
M₂ : Type uM₂
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
ψ : Dual R M₂
⊢ f.dualMap ψ ∈ (ker f).dualAnnihilator
-- Mathlib/RingTheory/Ideal/Height.lean
@[gcongr]
lemma Ideal.primeHeight_strict_mono {I J : Ideal R} [I.IsPrime] [J.IsPrime]
    (h : I < J) [I.FiniteHeight] :
    I.primeHeight < J.primeHeight

Proof state:
R : Type u_1
inst✝³ : CommRing R
I J : Ideal R
inst✝² : I.IsPrime
inst✝¹ : J.IsPrime
h : I < J
inst✝ : I.FiniteHeight
⊢ Order.height { asIdeal := I, isPrime := inst✝² } < Order.height { asIdeal := J, isPrime := inst✝¹ }

Tactic:
gcongr

Result:
case hfin
R : Type u_1
inst✝³ : CommRing R
I J : Ideal R
inst✝² : I.IsPrime
inst✝¹ : J.IsPrime
h : I < J
inst✝ : I.FiniteHeight
⊢ Order.height { asIdeal := I, isPrime := inst✝² } < ⊤

case hxy
R : Type u_1
inst✝³ : CommRing R
I J : Ideal R
inst✝² : I.IsPrime
inst✝¹ : J.IsPrime
h : I < J
inst✝ : I.FiniteHeight
⊢ { asIdeal := I, isPrime := inst✝² } < { asIdeal := J, isPrime := inst✝¹ }

Proof state:
case hxy
R : Type u_1
inst✝³ : CommRing R
I J : Ideal R
inst✝² : I.IsPrime
inst✝¹ : J.IsPrime
h : I < J
inst✝ : I.FiniteHeight
⊢ { asIdeal := I, isPrime := inst✝² } < { asIdeal := J, isPrime := inst✝¹ }

Tactic:
exact h

Result:
no goals

Proof state:
case hfin
R : Type u_1
inst✝³ : CommRing R
I J : Ideal R
inst✝² : I.IsPrime
inst✝¹ : J.IsPrime
h : I < J
inst✝ : I.FiniteHeight
⊢ Order.height { asIdeal := I, isPrime := inst✝² } < ⊤

Tactic:
exact I.primeHeight_ne_top.lt_top

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
I J : Ideal R
inst✝² : I.IsPrime
inst✝¹ : J.IsPrime
h : I < J
inst✝ : I.FiniteHeight
⊢ I.primeHeight < J.primeHeight

Tactic:
unfold primeHeight

Result:
R : Type u_1
inst✝³ : CommRing R
I J : Ideal R
inst✝² : I.IsPrime
inst✝¹ : J.IsPrime
h : I < J
inst✝ : I.FiniteHeight
⊢ Order.height { asIdeal := I, isPrime := inst✝² } < Order.height { asIdeal := J, isPrime := inst✝¹ }
-- Mathlib/Algebra/Squarefree/Basic.lean
theorem Squarefree.ne_zero [MonoidWithZero R] [Nontrivial R] {m : R} (hm : Squarefree (m : R)) :
    m ≠ 0

Proof state:
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
hm : Squarefree 0
⊢ False

Tactic:
exact not_squarefree_zero hm

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
m : R
hm : Squarefree m
⊢ m ≠ 0

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝¹ : MonoidWithZero R
inst✝ : Nontrivial R
hm : Squarefree 0
⊢ False
-- Mathlib/Data/List/OfFn.lean
theorem ofFn_succ' {n} (f : Fin (succ n) → α) :
    ofFn f = (ofFn fun i => f (Fin.castSucc i)).concat (f (Fin.last _))

Proof state:
case succ
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = (ofFn fun i => f i.castSucc).concat (f (Fin.last n))
f : Fin (n + 1).succ → α
⊢ ofFn f = (ofFn fun i => f i.castSucc).concat (f (Fin.last (n + 1)))

Tactic:
rw [ofFn_succ, IH, ofFn_succ, concat_cons, Fin.castSucc_zero]

Result:
case succ
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = (ofFn fun i => f i.castSucc).concat (f (Fin.last n))
f : Fin (n + 1).succ → α
⊢ f 0 :: (ofFn fun i => f i.castSucc.succ).concat (f (Fin.last n).succ) =
    f 0 :: (ofFn fun i => f i.succ.castSucc).concat (f (Fin.last (n + 1)))

Proof state:
case zero
α : Type u
f : Fin (succ 0) → α
⊢ [f 0] = [f (Fin.last 0)]

Tactic:
rfl

Result:
no goals

Proof state:
case zero
α : Type u
f : Fin (succ 0) → α
⊢ ofFn f = (ofFn fun i => f i.castSucc).concat (f (Fin.last 0))

Tactic:
rw [ofFn_zero, concat_nil, ofFn_succ, ofFn_zero]

Result:
case zero
α : Type u
f : Fin (succ 0) → α
⊢ [f 0] = [f (Fin.last 0)]

Proof state:
α : Type u
n : ℕ
f : Fin n.succ → α
⊢ ofFn f = (ofFn fun i => f i.castSucc).concat (f (Fin.last n))

Tactic:
induction' n with n IH

Result:
case zero
α : Type u
f : Fin (succ 0) → α
⊢ ofFn f = (ofFn fun i => f i.castSucc).concat (f (Fin.last 0))

case succ
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = (ofFn fun i => f i.castSucc).concat (f (Fin.last n))
f : Fin (n + 1).succ → α
⊢ ofFn f = (ofFn fun i => f i.castSucc).concat (f (Fin.last (n + 1)))

Proof state:
case succ
α : Type u
n : ℕ
IH : ∀ (f : Fin n.succ → α), ofFn f = (ofFn fun i => f i.castSucc).concat (f (Fin.last n))
f : Fin (n + 1).succ → α
⊢ f 0 :: (ofFn fun i => f i.castSucc.succ).concat (f (Fin.last n).succ) =
    f 0 :: (ofFn fun i => f i.succ.castSucc).concat (f (Fin.last (n + 1)))

Tactic:
congr

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/KLFun.lean
lemma klFun_eq_zero_iff (hx : 0 ≤ x) : klFun x = 0 ↔ x = 1

Proof state:
x : ℝ
hx : 0 ≤ x
h : klFun x = 0
⊢ x = 1

Tactic:
exact strictConvexOn_klFun.eq_of_isMinOn (isMinOn_iff.mpr fun y hy ↦ h ▸ klFun_nonneg hy)
  isMinOn_klFun hx (zero_le_one' ℝ)

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
h : x = 1
⊢ klFun x = 0

Tactic:
simp [klFun_apply, h]

Result:
no goals

Proof state:
x : ℝ
hx : 0 ≤ x
⊢ klFun x = 0 ↔ x = 1

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [klFun_apply, h]⟩

Result:
x : ℝ
hx : 0 ≤ x
h : klFun x = 0
⊢ x = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x

Proof state:
α : Type u_1
a : Array α
x : α
⊢ (a.push x)[a.size] = x

Tactic:
simp only [push, ← getElem_toList, List.concat_eq_append]

Result:
α : Type u_1
a : Array α
x : α
⊢ (a.toList ++ [x])[a.size] = x

Proof state:
α : Type u_1
a : Array α
x : α
⊢ (a.toList ++ [x])[a.size] = x

Tactic:
rw [List.getElem_append_right] <;> simp [← getElem_toList, Nat.zero_lt_one]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/IsInvertedBy.lean
theorem unop {W : MorphismProperty C} {L : Cᵒᵖ ⥤ Dᵒᵖ} (h : W.op.IsInvertedBy L) :
    W.IsInvertedBy L.unop := fun X Y f hf => by
  haveI := h f.op hf
  dsimp
  infer_instance

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : Cᵒᵖ ⥤ Dᵒᵖ
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
⊢ IsIso (L.unop.map f)

Tactic:
haveI := h f.op hf

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : Cᵒᵖ ⥤ Dᵒᵖ
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
this : IsIso (L.map f.op)
⊢ IsIso (L.unop.map f)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : Cᵒᵖ ⥤ Dᵒᵖ
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
this : IsIso (L.map f.op)
⊢ IsIso (L.unop.map f)

Tactic:
dsimp

Result:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : Cᵒᵖ ⥤ Dᵒᵖ
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
this : IsIso (L.map f.op)
⊢ IsIso (L.map f.op).unop

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
W : MorphismProperty C
L : Cᵒᵖ ⥤ Dᵒᵖ
h : W.op.IsInvertedBy L
X Y : C
f : X ⟶ Y
hf : W f
this : IsIso (L.map f.op)
⊢ IsIso (L.map f.op).unop

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem exists_inv_mem_iff_exists_mem {P : G → Prop} :
    (∃ x : G, x ∈ H ∧ P x⁻¹) ↔ ∃ x ∈ H, P x

Proof state:
case mpr
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
⊢ (∃ x ∈ H, P x) → ∃ x ∈ H, P x⁻¹

Tactic:
rintro ⟨x, x_in, hx⟩

Result:
case mpr.intro.intro
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
x : G
x_in : x ∈ H
hx : P x
⊢ ∃ x ∈ H, P x⁻¹

Proof state:
case mpr.intro.intro
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
x : G
x_in : x ∈ H
hx : P x
⊢ ∃ x ∈ H, P x⁻¹

Tactic:
exact ⟨x⁻¹, inv_mem x_in, by simp [hx]⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
P : G → Prop
x : G
x_in : x ∈ H
hx : P x
⊢ P x⁻¹⁻¹

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
theorem one : padicValInt p 1 = 0

Proof state:
p : ℕ
⊢ padicValInt p 1 = 0

Tactic:
simp [padicValInt]

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum₂_self {α : Type*} [CommRing α] (x : α) (n : ℕ) :
    ∑ i ∈ range n, x ^ i * x ^ (n - 1 - i) = n * x ^ (n - 1) :=
  calc
    ∑ i ∈ Finset.range n, x ^ i * x ^ (n - 1 - i) =
        ∑ i ∈ Finset.range n, x ^ (i + (n - 1 - i))

Proof state:
α : Type u_1
inst✝ : CommRing α
x : α
n : ℕ
⊢ ∑ i ∈ range n, x ^ i * x ^ (n - 1 - i) = ∑ i ∈ range n, x ^ (i + (n - 1 - i))

Tactic:
simp_rw [← pow_add]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommRing α
x : α
n : ℕ
⊢ #(range n) • x ^ (n - 1) = ↑n * x ^ (n - 1)

Tactic:
rw [Finset.card_range, nsmul_eq_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Count.lean
theorem count_singleton' {a : α} (ha : MeasurableSet ({a} : Set α)) : count ({a} : Set α) = 1

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
a : α
ha : MeasurableSet {a}
⊢ ↑{a}.toFinset.card = 1

Tactic:
simp [@toFinset_card _ _ (Set.finite_singleton a).fintype,
  @Fintype.card_unique _ _ (Set.finite_singleton a).fintype]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
a : α
ha : MeasurableSet {a}
⊢ count {a} = 1

Tactic:
rw [count_apply_finite' (Set.finite_singleton a) ha, Set.Finite.toFinset]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
a : α
ha : MeasurableSet {a}
⊢ ↑{a}.toFinset.card = 1
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem associated_zero_iff_eq_zero [MonoidWithZero M] (a : M) : a ~ᵤ 0 ↔ a = 0 :=
  Iff.intro
    (fun h => by
      let ⟨u, h⟩ := h.symm
      simpa using h.symm)
    fun h => h ▸ Associated.refl a

Proof state:
M : Type u_1
inst✝ : MonoidWithZero M
a : M
h : a ~ᵤ 0
⊢ a = 0

Tactic:
let ⟨u, h⟩ := h.symm

Result:
M : Type u_1
inst✝ : MonoidWithZero M
a : M
h✝ : a ~ᵤ 0
u : Mˣ
h : 0 * ↑u = a
⊢ a = 0

Proof state:
M : Type u_1
inst✝ : MonoidWithZero M
a : M
h✝ : a ~ᵤ 0
u : Mˣ
h : 0 * ↑u = a
⊢ a = 0

Tactic:
simpa using h.symm

Result:
no goals
-- Mathlib/MeasureTheory/Covering/VitaliFamily.lean
theorem measure_le_tsum_of_absolutelyContinuous [SecondCountableTopology X] {ρ : Measure X}
    (hρ : ρ ≪ μ) : ρ s ≤ ∑' p : h.index, ρ (h.covering p) :=
  calc
    ρ s ≤ ρ ((s \ ⋃ p ∈ h.index, h.covering p) ∪ ⋃ p ∈ h.index, h.covering p) :=
      measure_mono (by simp only [subset_union_left, diff_union_self])
    _ ≤ ρ (s \ ⋃ p ∈ h.index, h.covering p) + ρ (⋃ p ∈ h.index, h.covering p) :=
      (measure_union_le _ _)
    _ = ∑' p : h.index, ρ (h.covering p)

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
inst✝ : SecondCountableTopology X
ρ : Measure X
hρ : ρ ≪ μ
⊢ s ⊆ (s \ ⋃ p ∈ h.index, h.covering p) ∪ ⋃ p ∈ h.index, h.covering p

Tactic:
simp only [subset_union_left, diff_union_self]

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
inst✝ : SecondCountableTopology X
ρ : Measure X
hρ : ρ ≪ μ
⊢ ρ (s \ ⋃ p ∈ h.index, h.covering p) + ρ (⋃ p ∈ h.index, h.covering p) = ∑' (p : ↑h.index), ρ (h.covering ↑p)

Tactic:
rw [hρ h.measure_diff_biUnion, zero_add,
  measure_biUnion h.index_countable h.covering_disjoint fun x hx => h.measurableSet_u hx]

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem IsSeparable.of_algHom {x : E} (h : IsSeparable F (f x)) : IsSeparable F x

Proof state:
F : Type u_1
inst✝⁴ : Field F
E : Type u_3
E' : Type u_4
inst✝³ : Field E
inst✝² : Field E'
inst✝¹ : Algebra F E
inst✝ : Algebra F E'
f : E →ₐ[F] E'
x : E
h : IsSeparable F (f x)
x✝ : Algebra E E' := f.toAlgebra
⊢ IsSeparable F x

Tactic:
haveI : IsScalarTower F E E' := IsScalarTower.of_algebraMap_eq fun x => (f.commutes x).symm

Result:
F : Type u_1
inst✝⁴ : Field F
E : Type u_3
E' : Type u_4
inst✝³ : Field E
inst✝² : Field E'
inst✝¹ : Algebra F E
inst✝ : Algebra F E'
f : E →ₐ[F] E'
x : E
h : IsSeparable F (f x)
x✝ : Algebra E E' := f.toAlgebra
this : IsScalarTower F E E'
⊢ IsSeparable F x

Proof state:
F : Type u_1
inst✝⁴ : Field F
E : Type u_3
E' : Type u_4
inst✝³ : Field E
inst✝² : Field E'
inst✝¹ : Algebra F E
inst✝ : Algebra F E'
f : E →ₐ[F] E'
x : E
h : IsSeparable F (f x)
x✝ : Algebra E E' := f.toAlgebra
this : IsScalarTower F E E'
⊢ IsSeparable F x

Tactic:
exact h.tower_bot

Result:
no goals

Proof state:
F : Type u_1
inst✝⁴ : Field F
E : Type u_3
E' : Type u_4
inst✝³ : Field E
inst✝² : Field E'
inst✝¹ : Algebra F E
inst✝ : Algebra F E'
f : E →ₐ[F] E'
x : E
h : IsSeparable F (f x)
⊢ IsSeparable F x

Tactic:
let _ : Algebra E E' := RingHom.toAlgebra f.toRingHom

Result:
F : Type u_1
inst✝⁴ : Field F
E : Type u_3
E' : Type u_4
inst✝³ : Field E
inst✝² : Field E'
inst✝¹ : Algebra F E
inst✝ : Algebra F E'
f : E →ₐ[F] E'
x : E
h : IsSeparable F (f x)
x✝ : Algebra E E' := f.toAlgebra
⊢ IsSeparable F x
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem foldlM_eq [Monad m] (f : δ → α → β → m δ) (init l) :
    foldlM f init l = l.toList.foldlM (fun d (a, b) => f d a b) init

Proof state:
m : Type u_1 → Type u_2
δ : Type u_1
α : Type u_3
β : Type u_4
inst✝ : Monad m
f : δ → α → β → m δ
init : δ
l : AssocList α β
⊢ foldlM f init l =
    List.foldlM
      (fun d x =>
        match x with
        | (a, b) => f d a b)
      init l.toList

Tactic:
induction l generalizing init <;> simp [*, foldlM]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_succ' [AddMonoidWithOne α] (n) : (succ' n : α) = n + 1

Proof state:
α : Type u_1
inst✝ : AddMonoidWithOne α
n : Num
⊢ ↑n.succ' = ↑n + 1

Tactic:
rw [← PosNum.cast_to_nat, succ'_to_nat, Nat.cast_add_one, cast_to_nat]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem _root_.MeasureTheory.OuterMeasure.toMeasure_top :
    (⊤ : OuterMeasure α).toMeasure (by rw [OuterMeasure.top_caratheodory]; exact le_top) =
      (⊤ : Measure α) :=
  toOuterMeasure_toMeasure (μ := ⊤)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
⊢ m0 ≤ ⊤.caratheodory

Tactic:
rw [OuterMeasure.top_caratheodory]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
⊢ m0 ≤ ⊤

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
⊢ m0 ≤ ⊤

Tactic:
exact le_top

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem eq_bot_of_subsingleton [Subsingleton H] : H = ⊥

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Subsingleton ↥H
y : G
hy : y ∈ H
⊢ y = 1

Tactic:
rw [← Subgroup.coe_mk H y hy, Subsingleton.elim (⟨y, hy⟩ : H) 1, Subgroup.coe_one]

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Subsingleton ↥H
⊢ H = ⊥

Tactic:
rw [Subgroup.eq_bot_iff_forall]

Result:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Subsingleton ↥H
⊢ ∀ x ∈ H, x = 1

Proof state:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Subsingleton ↥H
⊢ ∀ x ∈ H, x = 1

Tactic:
intro y hy

Result:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : Subsingleton ↥H
y : G
hy : y ∈ H
⊢ y = 1