harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Shift/Basic.lean
lemma shiftFunctorComm_eq (i j k : A) (h : i + j = k) :
    shiftFunctorComm C i j = (shiftFunctorAdd' C i j k h).symm ≪≫
      shiftFunctorAdd' C j i k (by rw [add_comm j i, h])

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ shiftFunctorComm C i j = (shiftFunctorAdd C i j).symm ≪≫ shiftFunctorAdd' C j i (i + j) ⋯

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j k : A
h : i + j = k
⊢ shiftFunctorComm C i j = (shiftFunctorAdd' C i j k h).symm ≪≫ shiftFunctorAdd' C j i k ⋯

Tactic:
subst h

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ shiftFunctorComm C i j = (shiftFunctorAdd' C i j (i + j) ⋯).symm ≪≫ shiftFunctorAdd' C j i (i + j) ⋯

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j k : A
h : i + j = k
⊢ j + i = k

Tactic:
rw [add_comm j i, h]

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ shiftFunctorComm C i j = (shiftFunctorAdd' C i j (i + j) ⋯).symm ≪≫ shiftFunctorAdd' C j i (i + j) ⋯

Tactic:
rw [shiftFunctorAdd'_eq_shiftFunctorAdd]

Result:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
i j : A
⊢ shiftFunctorComm C i j = (shiftFunctorAdd C i j).symm ≪≫ shiftFunctorAdd' C j i (i + j) ⋯
-- Mathlib/Logic/Equiv/Defs.lean
theorem Perm.coe_subsingleton {α : Type*} [Subsingleton α] (e : Perm α) : (e : α → α) = id

Proof state:
α : Type u_1
inst✝ : Subsingleton α
e : Perm α
⊢ ⇑e = id

Tactic:
rw [Perm.subsingleton_eq_refl e, coe_refl]

Result:
no goals
-- Mathlib/Topology/Order/Basic.lean
theorem nhdsLE_eq_iInf_principal [TopologicalSpace α] [Preorder α] [OrderTopology α] {a : α}
    (ha : ∃ l, l < a) : 𝓝[≤] a = ⨅ l < a, 𝓟 (Ioc l a)

Proof state:
α : Type u
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
ha : ∃ l, l < a
⊢ 𝓝[≤] a = ⨅ l, ⨅ (_ : l < a), 𝓟 (Ioc l a)

Tactic:
simp only [nhdsLE_eq_iInf_inf_principal, biInf_inf ha, inf_principal, Ioi_inter_Iic]

Result:
no goals
-- Mathlib/Data/Part.lean
theorem mem_restrict (p : Prop) (o : Part α) (h : p → o.Dom) (a : α) :
    a ∈ restrict p o h ↔ p ∧ a ∈ o

Proof state:
case mpr.intro.intro
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
w✝ : o.Dom
h₂ : o.get w✝ = a
⊢ ∃ (h_1 : p), o.get ⋯ = a

Tactic:
exact ⟨h₀, h₂⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ (h_1 : p), o.get ⋯ = a) → p ∧ ∃ (h : o.Dom), o.get h = a

Tactic:
rintro ⟨h₀, h₁⟩

Result:
case mp.intro
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
h₁ : o.get ⋯ = a
⊢ p ∧ ∃ (h : o.Dom), o.get h = a

Proof state:
case mp.intro
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
h₁ : o.get ⋯ = a
⊢ p ∧ ∃ (h : o.Dom), o.get h = a

Tactic:
exact ⟨h₀, ⟨_, h₁⟩⟩

Result:
no goals

Proof state:
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ a ∈ restrict p o h ↔ p ∧ a ∈ o

Tactic:
dsimp [restrict, mem_eq]

Result:
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ (h_1 : p), o.get ⋯ = a) ↔ p ∧ ∃ (h : o.Dom), o.get h = a

Proof state:
case mpr
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (p ∧ ∃ (h : o.Dom), o.get h = a) → ∃ (h_1 : p), o.get ⋯ = a

Tactic:
rintro ⟨h₀, _, h₂⟩

Result:
case mpr.intro.intro
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
h₀ : p
w✝ : o.Dom
h₂ : o.get w✝ = a
⊢ ∃ (h_1 : p), o.get ⋯ = a

Proof state:
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ (h_1 : p), o.get ⋯ = a) ↔ p ∧ ∃ (h : o.Dom), o.get h = a

Tactic:
constructor

Result:
case mp
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (∃ (h_1 : p), o.get ⋯ = a) → p ∧ ∃ (h : o.Dom), o.get h = a

case mpr
α : Type u_1
p : Prop
o : Part α
h : p → o.Dom
a : α
⊢ (p ∧ ∃ (h : o.Dom), o.get h = a) → ∃ (h_1 : p), o.get ⋯ = a
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem nonempty (g : Perm α) : Nonempty (Basis g)

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
this : ∀ (c : { x // x ∈ g.cycleFactorsFinset }), (↑c).support.Nonempty
⊢ Nonempty g.Basis

Tactic:
exact ⟨fun c ↦ (this c).choose, fun c ↦ (this c).choose_spec⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Nonempty g.Basis

Tactic:
have (c : g.cycleFactorsFinset) : c.val.support.Nonempty :=
  IsCycle.nonempty_support (mem_cycleFactorsFinset_iff.mp c.prop).1

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
this : ∀ (c : { x // x ∈ g.cycleFactorsFinset }), (↑c).support.Nonempty
⊢ Nonempty g.Basis
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem append_inj' {s₁ s₂ t₁ t₂ : Array α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : t₁.size = t₂.size) :
    s₁ = s₂ ∧ t₁ = t₂ :=
  append_inj h <| @Nat.add_right_cancel _ t₁.size _ <| by
    let hap := congrArg size h; simp only [size_append, ← hl] at hap; exact hap

Proof state:
α : Type u_1
s₁ s₂ t₁ t₂ : Array α
h : s₁ ++ t₁ = s₂ ++ t₂
hl : t₁.size = t₂.size
⊢ s₁.size + t₁.size = s₂.size + t₁.size

Tactic:
let hap := congrArg size h

Result:
α : Type u_1
s₁ s₂ t₁ t₂ : Array α
h : s₁ ++ t₁ = s₂ ++ t₂
hl : t₁.size = t₂.size
hap : (s₁ ++ t₁).size = (s₂ ++ t₂).size := congrArg size h
⊢ s₁.size + t₁.size = s₂.size + t₁.size

Proof state:
α : Type u_1
s₁ s₂ t₁ t₂ : Array α
h : s₁ ++ t₁ = s₂ ++ t₂
hl : t₁.size = t₂.size
hap : s₁.size + t₁.size = s₂.size + t₁.size
⊢ s₁.size + t₁.size = s₂.size + t₁.size

Tactic:
exact hap

Result:
no goals

Proof state:
α : Type u_1
s₁ s₂ t₁ t₂ : Array α
h : s₁ ++ t₁ = s₂ ++ t₂
hl : t₁.size = t₂.size
hap : (s₁ ++ t₁).size = (s₂ ++ t₂).size := congrArg size h
⊢ s₁.size + t₁.size = s₂.size + t₁.size

Tactic:
simp only [size_append, ← hl] at hap

Result:
α : Type u_1
s₁ s₂ t₁ t₂ : Array α
h : s₁ ++ t₁ = s₂ ++ t₂
hl : t₁.size = t₂.size
hap : s₁.size + t₁.size = s₂.size + t₁.size
⊢ s₁.size + t₁.size = s₂.size + t₁.size
-- Mathlib/Topology/UniformSpace/Separation.lean
theorem map_unique {f : α → β} (hf : UniformContinuous f)
    {g : SeparationQuotient α → SeparationQuotient β} (comm : mk ∘ f = g ∘ mk) : map f = g

Proof state:
case h.mk
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : UniformContinuous f
g : SeparationQuotient α → SeparationQuotient β
comm : mk ∘ f = g ∘ mk
x✝ : SeparationQuotient α
a : α
⊢ map f (Quot.mk (⇑(inseparableSetoid α)) a) = g (Quot.mk (⇑(inseparableSetoid α)) a)

Tactic:
calc
  map f ⟦a⟧ = ⟦f a⟧ := map_mk hf a
  _ = g ⟦a⟧ := congr_fun comm a

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : UniformContinuous f
g : SeparationQuotient α → SeparationQuotient β
comm : mk ∘ f = g ∘ mk
⊢ map f = g

Tactic:
ext ⟨a⟩

Result:
case h.mk
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α → β
hf : UniformContinuous f
g : SeparationQuotient α → SeparationQuotient β
comm : mk ∘ f = g ∘ mk
x✝ : SeparationQuotient α
a : α
⊢ map f (Quot.mk (⇑(inseparableSetoid α)) a) = g (Quot.mk (⇑(inseparableSetoid α)) a)
-- Mathlib/CategoryTheory/Sites/Preserves.lean
theorem isSheafFor_of_preservesProduct [PreservesLimit (Discrete.functor (fun x ↦ op (X x))) F] :
    (ofArrows X c.inj).IsSheafFor F

Proof state:
C : Type u
inst✝² : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
α : Type
X : α → C
c : Cofan X
hc : IsColimit c
inst✝¹ : (ofArrows X c.inj).hasPullbacks
inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F
this : HasCoproduct X
hi :
  ∀ (b : ∏ᶜ fun b => F.obj (op (X b))),
    ∃! a,
      (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫
            Equalizer.Presieve.Arrows.forkMap F X c.inj)
          a =
        b
b : Equalizer.Presieve.Arrows.FirstObj F X
a✝ : Equalizer.Presieve.Arrows.firstMap F X c.inj b = Equalizer.Presieve.Arrows.secondMap F X c.inj b
t : F.obj (∏ᶜ fun x => op (X x))
ht₁ :
  (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫
        Equalizer.Presieve.Arrows.forkMap F X c.inj)
      t =
    b
ht₂ :
  ∀ (y : F.obj (∏ᶜ fun x => op (X x))),
    (fun a =>
          (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫
                Equalizer.Presieve.Arrows.forkMap F X c.inj)
              a =
            b)
        y →
      y = t
y : F.obj (op c.pt)
hy : (fun x => Equalizer.Presieve.Arrows.forkMap F X c.inj x = b) y
⊢ (fun a =>
      (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫
            Equalizer.Presieve.Arrows.forkMap F X c.inj)
          a =
        b)
    (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).hom y)

Tactic:
simp [← hy]

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
theorem pow_le_iff_le_log {b : ℕ} (hb : 1 < b) {x y : ℕ} (hy : y ≠ 0) :
    b ^ x ≤ y ↔ x ≤ log b y

Proof state:
case h.succ
b : ℕ
hb : 1 < b
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
⊢ b ^ (x + 1) ≤ y ↔ x + 1 ≤ if h : b ≤ y ∧ 1 < b then log b (y / b) + 1 else 0

Tactic:
split_ifs with h

Result:
case pos
b : ℕ
hb : 1 < b
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
h : b ≤ y ∧ 1 < b
⊢ b ^ (x + 1) ≤ y ↔ x + 1 ≤ log b (y / b) + 1

case neg
b : ℕ
hb : 1 < b
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
h : ¬(b ≤ y ∧ 1 < b)
⊢ b ^ (x + 1) ≤ y ↔ x + 1 ≤ 0

Proof state:
b : ℕ
hb : 1 < b
x y : ℕ
hy : y ≠ 0
⊢ b ^ x ≤ y ↔ x ≤ log b y

Tactic:
induction y using Nat.strong_induction_on generalizing x with | h y ih => ?_

Result:
case h
b : ℕ
hb : 1 < b
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
x : ℕ
hy : y ≠ 0
⊢ b ^ x ≤ y ↔ x ≤ log b y

Proof state:
case h.succ
b : ℕ
hb : 1 < b
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
⊢ b ^ (x + 1) ≤ y ↔ x + 1 ≤ log b y

Tactic:
rw [log]

Result:
case h.succ
b : ℕ
hb : 1 < b
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
⊢ b ^ (x + 1) ≤ y ↔ x + 1 ≤ if h : b ≤ y ∧ 1 < b then log b (y / b) + 1 else 0

Proof state:
case pos
b : ℕ
hb : 1 < b
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
h : b ≤ y ∧ 1 < b
⊢ b ^ (x + 1) ≤ y ↔ x + 1 ≤ log b (y / b) + 1

Tactic:
have b_pos : 0 < b := lt_of_succ_lt hb

Result:
case pos
b : ℕ
hb : 1 < b
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
h : b ≤ y ∧ 1 < b
b_pos : 0 < b
⊢ b ^ (x + 1) ≤ y ↔ x + 1 ≤ log b (y / b) + 1

Proof state:
case neg
b : ℕ
hb : 1 < b
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
h : ¬(b ≤ y ∧ 1 < b)
⊢ b ^ (x + 1) ≤ y ↔ x + 1 ≤ 0

Tactic:
exact iff_of_false (fun hby => h ⟨(le_self_pow x.succ_ne_zero _).trans hby, hb⟩)
  (not_succ_le_zero _)

Result:
no goals

Proof state:
case h.zero
b : ℕ
hb : 1 < b
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
⊢ b ^ 0 ≤ y ↔ 0 ≤ log b y

Tactic:
dsimp

Result:
case h.zero
b : ℕ
hb : 1 < b
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
⊢ 1 ≤ y ↔ 0 ≤ log b y

Proof state:
case pos
b : ℕ
hb : 1 < b
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
x : ℕ
h : b ≤ y ∧ 1 < b
b_pos : 0 < b
⊢ b ^ (x + 1) ≤ y ↔ x + 1 ≤ log b (y / b) + 1

Tactic:
rw [Nat.add_le_add_iff_right, ← ih (y / b) (div_lt_self
  (Nat.pos_iff_ne_zero.2 hy) hb) (Nat.div_pos h.1 b_pos).ne', le_div_iff_mul_le b_pos,
  pow_succ', Nat.mul_comm]

Result:
no goals

Proof state:
case h.zero
b : ℕ
hb : 1 < b
y : ℕ
ih : ∀ (m : ℕ), m < y → ∀ {x : ℕ}, m ≠ 0 → (b ^ x ≤ m ↔ x ≤ log b m)
hy : y ≠ 0
⊢ 1 ≤ y ↔ 0 ≤ log b y

Tactic:
omega

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sup_lt_of_lt_sdiff_left (h : y < z \ x) (hxz : x ≤ z) : x ⊔ y < z

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
⊢ x ⊔ y < z

Tactic:
rw [← sup_sdiff_cancel_right hxz]

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
⊢ x ⊔ y < x ⊔ z \ x

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
h' : x ⊔ z \ x ≤ x ⊔ y
⊢ z \ x ≤ y

Tactic:
rw [← sdiff_idem]

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
h' : x ⊔ z \ x ≤ x ⊔ y
⊢ (z \ x) \ x ≤ y

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
⊢ x ⊔ y < x ⊔ z \ x

Tactic:
refine (sup_le_sup_left h.le _).lt_of_not_le fun h' => h.not_le ?_

Result:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
h' : x ⊔ z \ x ≤ x ⊔ y
⊢ z \ x ≤ y

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
h : y < z \ x
hxz : x ≤ z
h' : x ⊔ z \ x ≤ x ⊔ y
⊢ (z \ x) \ x ≤ y

Tactic:
exact (sdiff_le_sdiff_of_sup_le_sup_left h').trans sdiff_le

Result:
no goals
-- Mathlib/NumberTheory/Transcendental/Lindemann/Init/AnalyticalPart.lean
theorem P_eq_integral_exp_mul_eval (f : ℂ[X]) (s : ℂ) :
    P f s = exp s * (s * ∫ x in (0)..1, exp (-(x • s)) * f.eval (x • s))

Proof state:
f : ℂ[X]
s : ℂ
⊢ LindemannWeierstrass.P f s = cexp s * (s * ∫ (x : ℝ) in 0 ..1, cexp (-(x • s)) * eval (x • s) f)

Tactic:
rw [integral_exp_mul_eval, mul_add, mul_neg, exp_neg, mul_inv_cancel_left₀ (exp_ne_zero s),
  neg_add_eq_sub, P]

Result:
no goals
-- Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean
theorem prod_smul
    [CommMonoid β] [CommMonoid α] [MulAction α β] [IsScalarTower α β β] [SMulCommClass α β β]
    (s : Finset β) (b : β → α) (f : β → β) :
    ∏ i ∈ s, b i • f i = (∏ i ∈ s, b i) • ∏ i ∈ s, f i

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid β
inst✝³ : CommMonoid α
inst✝² : MulAction α β
inst✝¹ : IsScalarTower α β β
inst✝ : SMulCommClass α β β
s : Finset β
b : β → α
f : β → β
⊢ ∏ i ∈ s, b i • f i = (∏ i ∈ s, b i) • ∏ i ∈ s, f i

Tactic:
induction s using Finset.cons_induction_on with
| h₁ =>  simp
| h₂ hj ih => rw [prod_cons, ih, smul_mul_smul_comm, ← prod_cons hj, ← prod_cons hj]

Result:
no goals

Proof state:
case h₂
α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid β
inst✝³ : CommMonoid α
inst✝² : MulAction α β
inst✝¹ : IsScalarTower α β β
inst✝ : SMulCommClass α β β
b : β → α
f : β → β
a✝ : β
s✝ : Finset β
hj : a✝ ∉ s✝
ih : ∏ i ∈ s✝, b i • f i = (∏ i ∈ s✝, b i) • ∏ i ∈ s✝, f i
⊢ ∏ i ∈ cons a✝ s✝ hj, b i • f i = (∏ i ∈ cons a✝ s✝ hj, b i) • ∏ i ∈ cons a✝ s✝ hj, f i

Tactic:
rw [prod_cons, ih, smul_mul_smul_comm, ← prod_cons hj, ← prod_cons hj]

Result:
no goals

Proof state:
case h₁
α : Type u_1
β : Type u_2
inst✝⁴ : CommMonoid β
inst✝³ : CommMonoid α
inst✝² : MulAction α β
inst✝¹ : IsScalarTower α β β
inst✝ : SMulCommClass α β β
b : β → α
f : β → β
⊢ ∏ i ∈ ∅, b i • f i = (∏ i ∈ ∅, b i) • ∏ i ∈ ∅, f i

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem subNat_one_succ (i : Fin (n + 1)) (h : 1 ≤ (i : Nat)) : (subNat 1 i h).succ = i

Proof state:
n : Nat
i : Fin (n + 1)
h : 1 ≤ ↑i
⊢ (subNat 1 i h).succ = i

Tactic:
ext

Result:
case h
n : Nat
i : Fin (n + 1)
h : 1 ≤ ↑i
⊢ ↑(subNat 1 i h).succ = ↑i

Proof state:
case h
n : Nat
i : Fin (n + 1)
h : 1 ≤ ↑i
⊢ ↑i - 1 + 1 = ↑i

Tactic:
omega

Result:
no goals

Proof state:
case h
n : Nat
i : Fin (n + 1)
h : 1 ≤ ↑i
⊢ ↑(subNat 1 i h).succ = ↑i

Tactic:
simp

Result:
case h
n : Nat
i : Fin (n + 1)
h : 1 ≤ ↑i
⊢ ↑i - 1 + 1 = ↑i
-- Mathlib/Algebra/Polynomial/BigOperators.lean
theorem natDegree_prod_le : (∏ i ∈ s, f i).natDegree ≤ ∑ i ∈ s, (f i).natDegree

Proof state:
R : Type u
ι : Type w
s : Finset ι
inst✝ : CommSemiring R
f : ι → R[X]
⊢ (∏ i ∈ s, f i).natDegree ≤ ∑ i ∈ s, (f i).natDegree

Tactic:
simpa using natDegree_multiset_prod_le (s.1.map f)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem index_union_le (K₁ K₂ : Compacts G) {V : Set G} (hV : (interior V).Nonempty) :
    index (K₁.1 ∪ K₂.1) V ≤ index K₁.1 V + index K₂.1 V

Proof state:
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
K₁ K₂ : Compacts G
V : Set G
hV : (interior V).Nonempty
s : Finset G
h1s : K₁.carrier ⊆ ⋃ g ∈ s, (fun h => g * h) ⁻¹' V
h2s : s.card = index K₁.carrier V
t : Finset G
h1t : K₂.carrier ⊆ ⋃ g ∈ t, (fun h => g * h) ⁻¹' V
h2t : t.card = index K₂.carrier V
⊢ K₂.carrier ⊆ ?m.15923

Tactic:
assumption

Result:
no goals
-- Mathlib/Computability/Encoding.lean
theorem decode_encodePosNum : ∀ n, decodePosNum (encodePosNum n) = n

Proof state:
⊢ ∀ (n : PosNum), decodePosNum (encodePosNum n) = n

Tactic:
intro n

Result:
n : PosNum
⊢ decodePosNum (encodePosNum n) = n

Proof state:
n : PosNum
⊢ decodePosNum (encodePosNum n) = n

Tactic:
induction' n with m hm m hm <;> unfold encodePosNum decodePosNum

Result:
case one

⊢ (if [] = [] then PosNum.one else (decodePosNum []).bit1) = PosNum.one

case bit1
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (if encodePosNum m = [] then PosNum.one else (decodePosNum (encodePosNum m)).bit1) = m.bit1

case bit0
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (decodePosNum (encodePosNum m)).bit0 = m.bit0

Proof state:
case bit1
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (if encodePosNum m = [] then PosNum.one else (decodePosNum (encodePosNum m)).bit1) = m.bit1

Tactic:
rw [hm]

Result:
case bit1
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (if encodePosNum m = [] then PosNum.one else m.bit1) = m.bit1

Proof state:
case bit1
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (if encodePosNum m = [] then PosNum.one else m.bit1) = m.bit1

Tactic:
exact if_neg (encodePosNum_nonempty m)

Result:
no goals

Proof state:
case one

⊢ (if [] = [] then PosNum.one else (decodePosNum []).bit1) = PosNum.one

Tactic:
rfl

Result:
no goals

Proof state:
case bit0
m : PosNum
hm : decodePosNum (encodePosNum m) = m
⊢ (decodePosNum (encodePosNum m)).bit0 = m.bit0

Tactic:
exact congr_arg PosNum.bit0 hm

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Bilinear.lean
theorem map₂_iSup_left (f : M →ₗ[R] N →ₗ[R] P) (s : ι → Submodule R M) (t : Submodule R N) :
    map₂ f (⨆ i, s i) t = ⨆ i, map₂ f (s i) t

Proof state:
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : ι → Submodule R M
t : Submodule R N
⊢ map₂ f (⨆ i, span R ↑(s i)) (span R ↑t) = ⨆ i, map₂ f (span R ↑(s i)) (span R ↑t)

Tactic:
simp_rw [map₂_span_span, ← span_iUnion, map₂_span_span, Set.image2_iUnion_left]

Result:
no goals

Proof state:
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : ι → Submodule R M
t : Submodule R N
⊢ map₂ f (⨆ i, s i) t = ⨆ i, map₂ f (s i) t

Tactic:
suffices map₂ f (⨆ i, span R (s i : Set M)) (span R t) = ⨆ i, map₂ f (span R (s i)) (span R t) by
  simpa only [span_eq] using this

Result:
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : ι → Submodule R M
t : Submodule R N
⊢ map₂ f (⨆ i, span R ↑(s i)) (span R ↑t) = ⨆ i, map₂ f (span R ↑(s i)) (span R ↑t)

Proof state:
ι : Sort uι
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
s : ι → Submodule R M
t : Submodule R N
this : map₂ f (⨆ i, span R ↑(s i)) (span R ↑t) = ⨆ i, map₂ f (span R ↑(s i)) (span R ↑t)
⊢ map₂ f (⨆ i, s i) t = ⨆ i, map₂ f (s i) t

Tactic:
simpa only [span_eq] using this

Result:
no goals
-- Mathlib/RingTheory/Finiteness/TensorProduct.lean
theorem exists_fg_le_eq_rTensor_inclusion (x : I ⊗ M) :
    ∃ (J : Submodule R N) (_ : J.FG) (hle : J ≤ I) (y : J ⊗ M),
      x = rTensor M (J.inclusion hle) y

Proof state:
case intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
I : Submodule R N
J : Submodule R ↥I
fg : J.FG
y : ↥J ⊗[R] M
⊢ ∃ J_1, ∃ (_ : J_1.FG) (hle : J_1 ≤ I), ∃ y_1, (rTensor M J.subtype) y = (rTensor M (inclusion hle)) y_1

Tactic:
refine ⟨J.map I.subtype, fg.map _, I.map_subtype_le J, rTensor M (I.subtype.submoduleMap J) y, ?_⟩

Result:
case intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
I : Submodule R N
J : Submodule R ↥I
fg : J.FG
y : ↥J ⊗[R] M
⊢ (rTensor M J.subtype) y = (rTensor M (inclusion ⋯)) ((rTensor M (I.subtype.submoduleMap J)) y)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
I : Submodule R N
x : ↥I ⊗[R] M
⊢ ∃ J, ∃ (_ : J.FG) (hle : J ≤ I), ∃ y, x = (rTensor M (inclusion hle)) y

Tactic:
obtain ⟨J, fg, y, rfl⟩ := exists_fg_le_eq_rTensor_subtype x

Result:
case intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
I : Submodule R N
J : Submodule R ↥I
fg : J.FG
y : ↥J ⊗[R] M
⊢ ∃ J_1, ∃ (_ : J_1.FG) (hle : J_1 ≤ I), ∃ y_1, (rTensor M J.subtype) y = (rTensor M (inclusion hle)) y_1

Proof state:
case intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
I : Submodule R N
J : Submodule R ↥I
fg : J.FG
y : ↥J ⊗[R] M
⊢ (rTensor M J.subtype) y = (rTensor M (inclusion ⋯ ∘ₗ I.subtype.submoduleMap J)) y

Tactic:
rfl

Result:
no goals

Proof state:
case intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
I : Submodule R N
J : Submodule R ↥I
fg : J.FG
y : ↥J ⊗[R] M
⊢ (rTensor M J.subtype) y = (rTensor M (inclusion ⋯)) ((rTensor M (I.subtype.submoduleMap J)) y)

Tactic:
rw [← LinearMap.rTensor_comp_apply]

Result:
case intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
I : Submodule R N
J : Submodule R ↥I
fg : J.FG
y : ↥J ⊗[R] M
⊢ (rTensor M J.subtype) y = (rTensor M (inclusion ⋯ ∘ₗ I.subtype.submoduleMap J)) y
-- Mathlib/Data/Finset/Card.lean
lemma le_card_of_inj_on_range (f : ℕ → α) (hf : ∀ i < n, f i ∈ s)
    (f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j) : n ≤ #s :=
  calc
    n = #(range n) := (card_range n).symm
    _ ≤ #s := card_le_card_of_injOn f (by simpa only [mem_range]) (by simpa)

Proof state:
α : Type u_1
s : Finset α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
⊢ ∀ a ∈ range n, f a ∈ s

Tactic:
simpa only [mem_range]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
n : ℕ
f : ℕ → α
hf : ∀ i < n, f i ∈ s
f_inj : ∀ i < n, ∀ j < n, f i = f j → i = j
⊢ Set.InjOn f ↑(range n)

Tactic:
simpa

Result:
no goals