harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Game/PGame.lean
theorem Subsequent.moveLeft_mk_right {xL : xl → PGame} {i : xr} (xR : xr → PGame) (j) :
    Subsequent ((xR i).moveLeft j) (mk xl xr xL xR)

Proof state:
xl xr : Type u
xL : xl → PGame
i : xr
xR : xr → PGame
j : (xR i).LeftMoves
⊢ ((xR i).moveLeft j).Subsequent (mk xl xr xL xR)

Tactic:
pgame_wf_tac

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Comon_.lean
theorem counit_comul_hom {Z : C} (f : M.X ⟶ Z) : M.comul ≫ (M.counit ⊗ f) = f ≫ (λ_ Z).inv

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
M : Comon_ C
Z : C
f : M.X ⟶ Z
⊢ M.comul ≫ (M.counit ⊗ f) = f ≫ (λ_ Z).inv

Tactic:
rw [leftUnitor_inv_naturality, tensorHom_def, counit_comul_assoc]

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
protected lemma add_sub_cancel (hts : t ≤ s) : s - t + t = s

Proof state:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
hts : t ≤ s
a : α
⊢ count a (s - t + t) = count a s

Tactic:
simp [Nat.sub_add_cancel <| count_le_of_le _ hts]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
hts : t ≤ s
⊢ s - t + t = s

Tactic:
ext a

Result:
case a
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
hts : t ≤ s
a : α
⊢ count a (s - t + t) = count a s
-- Mathlib/Order/Filter/Pointwise.lean
theorem isUnit_iff_singleton : IsUnit f ↔ ∃ a, f = pure a

Proof state:
α : Type u_2
inst✝ : Group α
f : Filter α
⊢ IsUnit f ↔ ∃ a, f = pure a

Tactic:
simp only [isUnit_iff, Group.isUnit, and_true]

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean
lemma directSumRight_comp_rTensor (f : M₁' →ₗ[R] M₂'):
    (directSumRight R M₂' M₁).toLinearMap ∘ₗ f.rTensor _ =
      (lmap fun _ ↦ f.rTensor _) ∘ₗ directSumRight R M₁' M₁

Proof state:
R : Type u
inst✝⁷ : CommSemiring R
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₁'
inst✝³ : AddCommMonoid M₂'
inst✝² : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝¹ : Module R M₁'
inst✝ : Module R M₂'
f : M₁' →ₗ[R] M₂'
⊢ ↑(directSumRight R M₂' M₁) ∘ₗ rTensor (⨁ (i : ι₁), M₁ i) f =
    (lmap fun x => rTensor (M₁ x) f) ∘ₗ ↑(directSumRight R M₁' M₁)

Tactic:
ext

Result:
case a.h.H.h.w
R : Type u
inst✝⁷ : CommSemiring R
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₁'
inst✝³ : AddCommMonoid M₂'
inst✝² : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝¹ : Module R M₁'
inst✝ : Module R M₂'
f : M₁' →ₗ[R] M₂'
x✝¹ : M₁'
i✝¹ : ι₁
x✝ : M₁ i✝¹
i✝ : ι₁
⊢ (((AlgebraTensorModule.curry (↑(directSumRight R M₂' M₁) ∘ₗ rTensor (⨁ (i : ι₁), M₁ i) f)) x✝¹ ∘ₗ lof R ι₁ M₁ i✝¹) x✝)
      i✝ =
    (((AlgebraTensorModule.curry ((lmap fun x => rTensor (M₁ x) f) ∘ₗ ↑(directSumRight R M₁' M₁))) x✝¹ ∘ₗ
          lof R ι₁ M₁ i✝¹)
        x✝)
      i✝

Proof state:
case a.h.H.h.w
R : Type u
inst✝⁷ : CommSemiring R
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₁'
inst✝³ : AddCommMonoid M₂'
inst✝² : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝¹ : Module R M₁'
inst✝ : Module R M₂'
f : M₁' →ₗ[R] M₂'
x✝¹ : M₁'
i✝¹ : ι₁
x✝ : M₁ i✝¹
i✝ : ι₁
⊢ (((AlgebraTensorModule.curry (↑(directSumRight R M₂' M₁) ∘ₗ rTensor (⨁ (i : ι₁), M₁ i) f)) x✝¹ ∘ₗ lof R ι₁ M₁ i✝¹) x✝)
      i✝ =
    (((AlgebraTensorModule.curry ((lmap fun x => rTensor (M₁ x) f) ∘ₗ ↑(directSumRight R M₁' M₁))) x✝¹ ∘ₗ
          lof R ι₁ M₁ i✝¹)
        x✝)
      i✝

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem eq_mul_of_hasProd_ite {α β : Type*} [TopologicalSpace α] [CommMonoid α] [T2Space α]
    [ContinuousMul α] [DecidableEq β] {f : β → α} {a : α} (hf : HasProd f a) (b : β) (a' : α)
    (hf' : HasProd (fun n ↦ ite (n = b) 1 (f n)) a') : a = a' * f b

Proof state:
α : Type u_4
β : Type u_5
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a : α
hf : HasProd f a
b : β
a' : α
hf' : HasProd (fun n => if n = b then 1 else f n) a'
⊢ a = a' * f b

Tactic:
refine (mul_one a).symm.trans (hf.update' b 1 ?_)

Result:
α : Type u_4
β : Type u_5
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a : α
hf : HasProd f a
b : β
a' : α
hf' : HasProd (fun n => if n = b then 1 else f n) a'
⊢ HasProd (update f b 1) a'

Proof state:
case h.e'_5.h
α : Type u_4
β : Type u_5
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a : α
hf : HasProd f a
b : β
a' : α
hf' : HasProd (fun n => if n = b then 1 else f n) a'
x✝ : β
⊢ update f b 1 x✝ = if x✝ = b then 1 else f x✝

Tactic:
apply update_apply

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a : α
hf : HasProd f a
b : β
a' : α
hf' : HasProd (fun n => if n = b then 1 else f n) a'
⊢ HasProd (update f b 1) a'

Tactic:
convert hf'

Result:
case h.e'_5.h
α : Type u_4
β : Type u_5
inst✝⁴ : TopologicalSpace α
inst✝³ : CommMonoid α
inst✝² : T2Space α
inst✝¹ : ContinuousMul α
inst✝ : DecidableEq β
f : β → α
a : α
hf : HasProd f a
b : β
a' : α
hf' : HasProd (fun n => if n = b then 1 else f n) a'
x✝ : β
⊢ update f b 1 x✝ = if x✝ = b then 1 else f x✝
-- Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
theorem support_bernoulli : (bernoulli p h).support = { b | cond b (p ≠ 0) (p ≠ 1) }

Proof state:
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ b ∈ (bernoulli p h).support ↔ b ∈ {b | bif b then p ≠ 0 else p ≠ 1}

Tactic:
induction b

Result:
case false
p : ℝ≥0∞
h : p ≤ 1
⊢ false ∈ (bernoulli p h).support ↔ false ∈ {b | bif b then p ≠ 0 else p ≠ 1}

case true
p : ℝ≥0∞
h : p ≤ 1
⊢ true ∈ (bernoulli p h).support ↔ true ∈ {b | bif b then p ≠ 0 else p ≠ 1}

Proof state:
case false
p : ℝ≥0∞
h : p ≤ 1
⊢ p < 1 ↔ false ∈ {b | bif b then ¬p = 0 else ¬p = 1}

Tactic:
exact ⟨ne_of_lt, lt_of_le_of_ne h⟩

Result:
no goals

Proof state:
p : ℝ≥0∞
h : p ≤ 1
⊢ (bernoulli p h).support = {b | bif b then p ≠ 0 else p ≠ 1}

Tactic:
refine Set.ext fun b => ?_

Result:
p : ℝ≥0∞
h : p ≤ 1
b : Bool
⊢ b ∈ (bernoulli p h).support ↔ b ∈ {b | bif b then p ≠ 0 else p ≠ 1}

Proof state:
case true
p : ℝ≥0∞
h : p ≤ 1
⊢ true ∈ (bernoulli p h).support ↔ true ∈ {b | bif b then p ≠ 0 else p ≠ 1}

Tactic:
simp only [mem_support_iff, bernoulli_apply, Bool.cond_true, Set.mem_setOf_eq]

Result:
no goals

Proof state:
case false
p : ℝ≥0∞
h : p ≤ 1
⊢ false ∈ (bernoulli p h).support ↔ false ∈ {b | bif b then p ≠ 0 else p ≠ 1}

Tactic:
simp_rw [mem_support_iff, bernoulli_apply, Bool.cond_false, Ne, tsub_eq_zero_iff_le, not_le]

Result:
case false
p : ℝ≥0∞
h : p ≤ 1
⊢ p < 1 ↔ false ∈ {b | bif b then ¬p = 0 else ¬p = 1}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Basic.lean
theorem drop_eq_cast_extract (v : Vector α n) (m : Nat) :
    v.drop m = (v.extract m n).cast (by simp)

Proof state:
α : Type u_1
n : Nat
v : Vector α n
m : Nat
⊢ v.drop m = Vector.cast ⋯ (v.extract m)

Tactic:
simp [drop, extract, Vector.cast]

Result:
no goals

Proof state:
α : Type ?u.8421
n : Nat
v : Vector α n
m : Nat
⊢ min n n - m = n - m

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
@[deprecated exists_eq_of_iSup_eq_of_not_isSuccLimit (since := "2024-09-17")]
lemma exists_eq_of_iSup_eq_of_not_isLimit
    {ι : Type u} [hι : Nonempty ι] (f : ι → Cardinal.{v}) (hf : BddAbove (range f))
    (ω : Cardinal.{v}) (hω : ¬ ω.IsLimit)
    (h : ⨆ i : ι, f i = ω) : ∃ i, f i = ω

Proof state:
case refl
ι : Type u
hι : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
hω : ¬IsLimit 0
h : ⨆ i, f i = 0
e : ¬0 ≠ 0
⊢ f hι.some = 0

Tactic:
rw [← le_zero_iff] at h ⊢

Result:
case refl
ι : Type u
hι : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
hω : ¬IsLimit 0
h : ⨆ i, f i ≤ 0
e : ¬0 ≠ 0
⊢ f hι.some ≤ 0

Proof state:
ι : Type u
hι : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
ω : Cardinal.{v}
hω : ¬ω.IsLimit
h : ⨆ i, f i = ω
e : ¬ω ≠ 0
⊢ f hι.some = ω

Tactic:
cases not_not.mp e

Result:
case refl
ι : Type u
hι : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
hω : ¬IsLimit 0
h : ⨆ i, f i = 0
e : ¬0 ≠ 0
⊢ f hι.some = 0

Proof state:
case refl
ι : Type u
hι : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
hω : ¬IsLimit 0
h : ⨆ i, f i ≤ 0
e : ¬0 ≠ 0
⊢ f hι.some ≤ 0

Tactic:
exact (le_ciSup hf _).trans h

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean
theorem isIso_of_mono (h : IsKernelPair f a b) [Mono f] : IsIso a

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : Mono f
⊢ IsIso a

Tactic:
rw [←
  show _ = a from
    (Category.comp_id _).symm.trans
      ((IsKernelPair.id_of_mono f).isLimit.conePointUniqueUpToIso_inv_comp h.isLimit
        WalkingCospan.left)]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : Mono f
⊢ IsIso ((IsPullback.isLimit ⋯).conePointUniqueUpToIso (IsPullback.isLimit h)).inv

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a b : R ⟶ X
h : IsKernelPair f a b
inst✝ : Mono f
⊢ IsIso ((IsPullback.isLimit ⋯).conePointUniqueUpToIso (IsPullback.isLimit h)).inv

Tactic:
infer_instance

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem modify_eq_set_get? (f : α → α) :
    ∀ n (l : List α), l.modify f n = ((fun a => l.set n (f a)) <$> l.get? n).getD l
  | 0, l => by cases l <;> rfl
  | _+1, [] => rfl
  | n+1, b :: l =>
    (congrArg (cons _) (modify_eq_set_get? ..)).trans <| by cases h : l[n]? <;> simp [h]

Proof state:
α : Type u_1
f : α → α
n : Nat
b : α
l : List α
⊢ b :: ((fun a => l.set n (f a)) <$> l.get? n).getD l =
    ((fun a => (b :: l).set (n + 1) (f a)) <$> (b :: l).get? (n + 1)).getD (b :: l)

Tactic:
cases h : l[n]? <;> simp [h]

Result:
no goals

Proof state:
α : Type u_1
f : α → α
l : List α
⊢ modify f 0 l = ((fun a => l.set 0 (f a)) <$> l.get? 0).getD l

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem coe_piecewise : ⇑(x.piecewise y s) = s.piecewise x y

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
x y : Π₀ (i : ι), β i
s : Set ι
inst✝ : (i : ι) → Decidable (i ∈ s)
⊢ ⇑(x.piecewise y s) = s.piecewise ⇑x ⇑y

Tactic:
ext

Result:
case h
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
x y : Π₀ (i : ι), β i
s : Set ι
inst✝ : (i : ι) → Decidable (i ∈ s)
x✝ : ι
⊢ (x.piecewise y s) x✝ = s.piecewise (⇑x) (⇑y) x✝

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
x y : Π₀ (i : ι), β i
s : Set ι
inst✝ : (i : ι) → Decidable (i ∈ s)
x✝ : ι
⊢ (x.piecewise y s) x✝ = s.piecewise (⇑x) (⇑y) x✝

Tactic:
apply piecewise_apply

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem coeff_injective : Injective (coeff : SkewMonoidAlgebra k G → G → k)

Proof state:
case ofFinsupp.ofFinsupp
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
p q : G →₀ k
⊢ { toFinsupp := p }.coeff = { toFinsupp := q }.coeff → { toFinsupp := p } = { toFinsupp := q }

Tactic:
simp only [coeff, DFunLike.coe_fn_eq, imp_self, ofFinsupp.injEq]

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
⊢ Injective coeff

Tactic:
rintro ⟨p⟩ ⟨q⟩

Result:
case ofFinsupp.ofFinsupp
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
p q : G →₀ k
⊢ { toFinsupp := p }.coeff = { toFinsupp := q }.coeff → { toFinsupp := p } = { toFinsupp := q }
-- Mathlib/LinearAlgebra/AffineSpace/Independent.lean
lemma AffineIndependent.eq_zero_of_sum_eq_zero_subtype {s : Finset V}
    (hp : AffineIndependent k ((↑) : s → V)) {w : V → k} (hw₀ : ∑ x ∈ s, w x = 0)
    (hw₁ : ∑ x ∈ s, w x • x = 0) : ∀ x ∈ s, w x = 0

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hp : AffineIndependent k Subtype.val
w : V → k
hw₀ : ∑ x ∈ s.attach, w ↑x = 0
hw₁ : ∑ x ∈ s.attach, w ↑x • ↑x = 0
⊢ ∀ x ∈ s, w x = 0

Tactic:
exact fun x hx ↦ hp.eq_zero_of_sum_eq_zero hw₀ hw₁ ⟨x, hx⟩ (mem_univ _)

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hp : AffineIndependent k Subtype.val
w : V → k
hw₀ : ∑ x ∈ s, w x = 0
hw₁ : ∑ x ∈ s, w x • x = 0
⊢ ∀ x ∈ s, w x = 0

Tactic:
rw [← sum_attach] at hw₀ hw₁

Result:
k : Type u_1
V : Type u_2
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
s : Finset V
hp : AffineIndependent k Subtype.val
w : V → k
hw₀ : ∑ x ∈ s.attach, w ↑x = 0
hw₁ : ∑ x ∈ s.attach, w ↑x • ↑x = 0
⊢ ∀ x ∈ s, w x = 0
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem rank_pow_quot_aux [IsDedekindDomain S] [p.IsMaximal] [P.IsPrime] (hP0 : P ≠ ⊥)
    {i : ℕ} (hi : i < e) :
    Module.rank (R ⧸ p) (Ideal.map (Ideal.Quotient.mk (P ^ e)) (P ^ i)) =
      Module.rank (R ⧸ p) (S ⧸ P) +
        Module.rank (R ⧸ p) (Ideal.map (Ideal.Quotient.mk (P ^ e)) (P ^ (i + 1)))

Proof state:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
hfp : NeZero e
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i < e
⊢ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) =
    Module.rank (R ⧸ p) (↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ LinearMap.range (p.powQuotSuccInclusion P i)) +
      Module.rank (R ⧸ p) ↥(LinearMap.range (p.powQuotSuccInclusion P i))

Tactic:
exact (Submodule.rank_quotient_add_rank (LinearMap.range (powQuotSuccInclusion p P i))).symm

Result:
no goals

Proof state:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
hfp : NeZero e
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i < e
⊢ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) =
    Module.rank (R ⧸ p) (S ⧸ P) + Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ (i + 1)))

Tactic:
rw [← rank_range_of_injective _ (powQuotSuccInclusion_injective p P i),
  (quotientRangePowQuotSuccInclusionEquiv p P hP0 hi).symm.rank_eq]

Result:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
hfp : NeZero e
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i < e
⊢ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) =
    Module.rank (R ⧸ p) (↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ LinearMap.range (p.powQuotSuccInclusion P i)) +
      Module.rank (R ⧸ p) ↥(LinearMap.range (p.powQuotSuccInclusion P i))
-- Mathlib/Algebra/Module/Projective.lean
theorem Projective.of_ringEquiv {R S} [Semiring R] [Semiring S] {M N}
    [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module S N]
    (e₁ : R ≃+* S) (e₂ : M ≃ₛₗ[RingHomClass.toRingHom e₁] N)
    [Projective R M] : Projective S N

Proof state:
case h
R : Type u_8
S : Type u_9
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module S N
e₁ : R ≃+* S
e₂ : M ≃ₛₗ[↑e₁] N
inst✝ : Projective R M
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
x y a✝ : N
⊢ ((fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x)))) (x + y)) a✝ =
    ((fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x)))) x +
        (fun x => mapRange ⇑e₁ ⋯ ((equivCongrLeft ↑e₂) (f (e₂.symm x)))) y)
      a✝

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem toSet_sep (a : ZFSet) (p : ZFSet → Prop) :
    (ZFSet.sep p a).toSet = { x ∈ a.toSet | p x }

Proof state:
case h
a : ZFSet.{u_1}
p : ZFSet.{u_1} → Prop
x✝ : ZFSet.{u_1}
⊢ x✝ ∈ (ZFSet.sep p a).toSet ↔ x✝ ∈ {x | x ∈ a.toSet ∧ p x}

Tactic:
simp

Result:
no goals

Proof state:
a : ZFSet.{u_1}
p : ZFSet.{u_1} → Prop
⊢ (ZFSet.sep p a).toSet = {x | x ∈ a.toSet ∧ p x}

Tactic:
ext

Result:
case h
a : ZFSet.{u_1}
p : ZFSet.{u_1} → Prop
x✝ : ZFSet.{u_1}
⊢ x✝ ∈ (ZFSet.sep p a).toSet ↔ x✝ ∈ {x | x ∈ a.toSet ∧ p x}
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem insert_inj_on' (s : Finset α) : Set.InjOn (fun a => insert a s) (sᶜ : Finset α)

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn (fun a => insert a s) (↑s)ᶜ

Tactic:
exact s.insert_inj_on

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn (fun a => insert a s) ↑sᶜ

Tactic:
rw [coe_compl]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn (fun a => insert a s) (↑s)ᶜ
-- Mathlib/Data/Finset/Piecewise.lean
lemma piecewise_mem_set_pi (hf : f ∈ Set.pi t t') (hg : g ∈ Set.pi t t') :
    s.piecewise f g ∈ Set.pi t t'

Proof state:
ι : Type u_1
s : Finset ι
inst✝ : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
t : Set ι
t' : (i : ι) → Set (π i)
f g : (i : ι) → π i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
⊢ (↑s).piecewise f g ∈ t.pi t'

Tactic:
exact Set.piecewise_mem_pi (↑s) hf hg

Result:
no goals

Proof state:
ι : Type u_1
s : Finset ι
inst✝ : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
t : Set ι
t' : (i : ι) → Set (π i)
f g : (i : ι) → π i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
⊢ s.piecewise f g ∈ t.pi t'

Tactic:
classical rw [← piecewise_coe]; exact Set.piecewise_mem_pi (↑s) hf hg

Result:
no goals

Proof state:
ι : Type u_1
s : Finset ι
inst✝ : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
t : Set ι
t' : (i : ι) → Set (π i)
f g : (i : ι) → π i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
⊢ s.piecewise f g ∈ t.pi t'

Tactic:
rw [← piecewise_coe]

Result:
ι : Type u_1
s : Finset ι
inst✝ : (j : ι) → Decidable (j ∈ s)
π : ι → Type u_3
t : Set ι
t' : (i : ι) → Set (π i)
f g : (i : ι) → π i
hf : f ∈ t.pi t'
hg : g ∈ t.pi t'
⊢ (↑s).piecewise f g ∈ t.pi t'
-- Mathlib/Data/List/Basic.lean
theorem foldl_hom₂ (l : List ι) (f : α → β → γ) (op₁ : α → ι → α) (op₂ : β → ι → β)
    (op₃ : γ → ι → γ) (a : α) (b : β) (h : ∀ a b i, f (op₁ a i) (op₂ b i) = op₃ (f a b) i) :
    foldl op₃ (f a b) l = f (foldl op₁ a l) (foldl op₂ b l) :=
  Eq.symm <| by
    revert a b
    induction l <;> intros <;> [rfl; simp only [*, foldl]]

Proof state:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
⊢ ∀ (a : α) (b : β), f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) l

Tactic:
induction l <;> intros <;> [rfl; simp only [*, foldl]]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
a : α
b : β
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
⊢ f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) l

Tactic:
revert a b

Result:
ι : Type u_1
α : Type u
β : Type v
γ : Type w
l : List ι
f : α → β → γ
op₁ : α → ι → α
op₂ : β → ι → β
op₃ : γ → ι → γ
h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i
⊢ ∀ (a : α) (b : β), f (foldl op₁ a l) (foldl op₂ b l) = foldl op₃ (f a b) l
-- Mathlib/Algebra/GradedMonoid.lean
theorem list_prod_map_mem_graded {ι'} (l : List ι') (i : ι' → ι) (r : ι' → R)
    (h : ∀ j ∈ l, r j ∈ A (i j)) : (l.map r).prod ∈ A (l.map i).sum

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ j ∈ [], r j ∈ A (i j)
⊢ 1 ∈ A 0

Tactic:
exact one_mem_graded _

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ j ∈ l, r j ∈ A (i j)
⊢ (List.map r l).prod ∈ A (List.map i l).sum

Tactic:
match l with
| [] =>
  rw [List.map_nil, List.map_nil, List.prod_nil, List.sum_nil]
  exact one_mem_graded _
| head::tail =>
  rw [List.map_cons, List.map_cons, List.prod_cons, List.sum_cons]
  exact
    mul_mem_graded (h _ <| List.mem_cons_self _ _)
      (list_prod_map_mem_graded tail _ _ fun j hj => h _ <| List.mem_cons_of_mem _ hj)

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ j ∈ head :: tail, r j ∈ A (i j)
⊢ (List.map r (head :: tail)).prod ∈ A (List.map i (head :: tail)).sum

Tactic:
rw [List.map_cons, List.map_cons, List.prod_cons, List.sum_cons]

Result:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ j ∈ head :: tail, r j ∈ A (i j)
⊢ r head * (List.map r tail).prod ∈ A (i head + (List.map i tail).sum)

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ j ∈ [], r j ∈ A (i j)
⊢ (List.map r []).prod ∈ A (List.map i []).sum

Tactic:
rw [List.map_nil, List.map_nil, List.prod_nil, List.sum_nil]

Result:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
h : ∀ j ∈ [], r j ∈ A (i j)
⊢ 1 ∈ A 0

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝³ : SetLike S R
inst✝² : Monoid R
inst✝¹ : AddMonoid ι
A : ι → S
inst✝ : GradedMonoid A
ι' : Type u_4
l : List ι'
i : ι' → ι
r : ι' → R
head : ι'
tail : List ι'
h : ∀ j ∈ head :: tail, r j ∈ A (i j)
⊢ r head * (List.map r tail).prod ∈ A (i head + (List.map i tail).sum)

Tactic:
exact
  mul_mem_graded (h _ <| List.mem_cons_self _ _)
    (list_prod_map_mem_graded tail _ _ fun j hj => h _ <| List.mem_cons_of_mem _ hj)

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
lemma ceil_lt_two_mul (ha : 2⁻¹ < a) : ⌈a⌉ < 2 * a :=
  ceil_lt_mul one_lt_two (by norm_num at ha ⊢; exact ha)

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha : 1 / 2 < a
⊢ 1 / 2 < a

Tactic:
exact ha

Result:
no goals

Proof state:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha : 2⁻¹ < a
⊢ ↑⌈(2 - 1)⁻¹⌉ / 2 < a

Tactic:
norm_num at ha ⊢

Result:
k : Type u_4
inst✝¹ : LinearOrderedField k
inst✝ : FloorRing k
a : k
ha : 1 / 2 < a
⊢ 1 / 2 < a