harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Lie/Basic.lean
theorem mk_coe (f : L₁ →ₗ⁅R⁆ L₂) (h₁ h₂ h₃) : (⟨⟨⟨f, h₁⟩, h₂⟩, h₃⟩ : L₁ →ₗ⁅R⁆ L₂) = f

Proof state:
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h₁ : ∀ (x y : L₁), f (x + y) = f x + f y
h₂ :
  ∀ (m : R) (x : L₁),
    { toFun := ⇑f, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := ⇑f, map_add' := h₁ }.toFun x
h₃ :
  ∀ {x y : L₁},
    { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun ⁅x, y⁆ =
      ⁅{ toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun x,
        { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun y⁆
⊢ { toFun := ⇑f, map_add' := h₁, map_smul' := h₂, map_lie' := h₃ } = f

Tactic:
ext

Result:
case h
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h₁ : ∀ (x y : L₁), f (x + y) = f x + f y
h₂ :
  ∀ (m : R) (x : L₁),
    { toFun := ⇑f, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := ⇑f, map_add' := h₁ }.toFun x
h₃ :
  ∀ {x y : L₁},
    { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun ⁅x, y⁆ =
      ⁅{ toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun x,
        { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun y⁆
x✝ : L₁
⊢ { toFun := ⇑f, map_add' := h₁, map_smul' := h₂, map_lie' := h₃ } x✝ = f x✝

Proof state:
case h
R : Type u
L₁ : Type v
L₂ : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L₁
inst✝² : LieAlgebra R L₁
inst✝¹ : LieRing L₂
inst✝ : LieAlgebra R L₂
f : L₁ →ₗ⁅R⁆ L₂
h₁ : ∀ (x y : L₁), f (x + y) = f x + f y
h₂ :
  ∀ (m : R) (x : L₁),
    { toFun := ⇑f, map_add' := h₁ }.toFun (m • x) = (RingHom.id R) m • { toFun := ⇑f, map_add' := h₁ }.toFun x
h₃ :
  ∀ {x y : L₁},
    { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun ⁅x, y⁆ =
      ⁅{ toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun x,
        { toFun := ⇑f, map_add' := h₁, map_smul' := h₂ }.toFun y⁆
x✝ : L₁
⊢ { toFun := ⇑f, map_add' := h₁, map_smul' := h₂, map_lie' := h₃ } x✝ = f x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/Defs.lean
theorem lapply_comp_lsingle_same (a : α) : lapply a ∘ₗ lsingle a = (.id : M →ₗ[R] M)

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : α
⊢ lapply a ∘ₗ lsingle a = LinearMap.id

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : α
x✝ : M
⊢ (lapply a ∘ₗ lsingle a) x✝ = LinearMap.id x✝

Proof state:
case h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : α
x✝ : M
⊢ (lapply a ∘ₗ lsingle a) x✝ = LinearMap.id x✝

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem submatrix {M : Matrix n n R} (hM : M.PosSemidef) (e : m → n) :
    (M.submatrix e e).PosSemidef

Proof state:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosSemidef
e : m → n
⊢ (Matrix.submatrix 1 e id * M * Matrix.submatrix 1 id e).PosSemidef

Tactic:
simpa only [conjTranspose_submatrix, conjTranspose_one] using
  conjTranspose_mul_mul_same hM (Matrix.submatrix 1 id e)

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosSemidef
e : m → n
⊢ (M.submatrix e e).PosSemidef

Tactic:
rw [(by simp : M = 1 * M * 1), submatrix_mul (he₂ := Function.bijective_id),
  submatrix_mul (he₂ := Function.bijective_id), submatrix_id_id]

Result:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosSemidef
e : m → n
⊢ (Matrix.submatrix 1 e id * M * Matrix.submatrix 1 id e).PosSemidef

Proof state:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosSemidef
e : m → n
⊢ (M.submatrix e e).PosSemidef

Tactic:
classical
rw [(by simp : M = 1 * M * 1), submatrix_mul (he₂ := Function.bijective_id),
  submatrix_mul (he₂ := Function.bijective_id), submatrix_id_id]
simpa only [conjTranspose_submatrix, conjTranspose_one] using
  conjTranspose_mul_mul_same hM (Matrix.submatrix 1 id e)

Result:
no goals

Proof state:
m : Type u_1
n : Type u_2
R : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosSemidef
e : m → n
⊢ M = 1 * M * 1

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem isSeparable_ae_range (hf : AEStronglyMeasurable f μ) :
    ∃ t : Set β, IsSeparable t ∧ ∀ᵐ x ∂μ, f x ∈ t

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
hf : AEStronglyMeasurable f μ
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
⊢ f x ∈ range (AEStronglyMeasurable.mk f hf)

Tactic:
simp [hx]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
hf : AEStronglyMeasurable f μ
⊢ ∃ t, IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t

Tactic:
refine ⟨range (hf.mk f), hf.stronglyMeasurable_mk.isSeparable_range, ?_⟩

Result:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
hf : AEStronglyMeasurable f μ
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ range (AEStronglyMeasurable.mk f hf)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
hf : AEStronglyMeasurable f μ
⊢ ∀ᵐ (x : α) ∂μ, f x ∈ range (AEStronglyMeasurable.mk f hf)

Tactic:
filter_upwards [hf.ae_eq_mk] with x hx

Result:
case h
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
f : α → β
hf : AEStronglyMeasurable f μ
x : α
hx : f x = AEStronglyMeasurable.mk f hf x
⊢ f x ∈ range (AEStronglyMeasurable.mk f hf)
-- Mathlib/Algebra/Group/Semiconj/Basic.lean
@[to_additive (attr := simp)] lemma inv_right_iff : SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y

Proof state:
G : Type u_1
inst✝ : Group G
a x y : G
⊢ SemiconjBy a x⁻¹ y⁻¹ ↔ SemiconjBy a x y

Tactic:
rw [← inv_symm_left_iff, inv_inv_symm_iff]

Result:
no goals
-- Mathlib/Data/DFinsupp/Module.lean
theorem single_smul {i : ι} (c : γ) (x : β i) : single i (c • x) = c • single i x :=
  ext fun i => by
    simp only [smul_apply, single_apply]
    split_ifs with h
    · cases h; rfl
    · rw [smul_zero]

Proof state:
case pos.refl
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
i : ι
c : γ
x : β i
⊢ ⋯ ▸ (c • x) = c • ⋯ ▸ x

Tactic:
rfl

Result:
no goals

Proof state:
case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
i✝ : ι
c : γ
x : β i✝
i : ι
h : ¬i✝ = i
⊢ 0 = c • 0

Tactic:
rw [smul_zero]

Result:
no goals

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
i✝ : ι
c : γ
x : β i✝
i : ι
⊢ (single i✝ (c • x)) i = (c • single i✝ x) i

Tactic:
simp only [smul_apply, single_apply]

Result:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
i✝ : ι
c : γ
x : β i✝
i : ι
⊢ (if h : i✝ = i then ⋯ ▸ (c • x) else 0) = c • if h : i✝ = i then ⋯ ▸ x else 0

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
i✝ : ι
c : γ
x : β i✝
i : ι
⊢ (if h : i✝ = i then ⋯ ▸ (c • x) else 0) = c • if h : i✝ = i then ⋯ ▸ x else 0

Tactic:
split_ifs with h

Result:
case pos
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
i✝ : ι
c : γ
x : β i✝
i : ι
h : i✝ = i
⊢ ⋯ ▸ (c • x) = c • ⋯ ▸ x

case neg
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
i✝ : ι
c : γ
x : β i✝
i : ι
h : ¬i✝ = i
⊢ 0 = c • 0

Proof state:
case pos
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
i✝ : ι
c : γ
x : β i✝
i : ι
h : i✝ = i
⊢ ⋯ ▸ (c • x) = c • ⋯ ▸ x

Tactic:
cases h

Result:
case pos.refl
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : DecidableEq ι
inst✝² : Monoid γ
inst✝¹ : (i : ι) → AddMonoid (β i)
inst✝ : (i : ι) → DistribMulAction γ (β i)
i : ι
c : γ
x : β i
⊢ ⋯ ▸ (c • x) = c • ⋯ ▸ x
-- Mathlib/Data/Finset/PImage.lean
theorem pimage_empty : pimage f ∅ = ∅

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α →. β
inst✝ : (x : α) → Decidable (f x).Dom
a✝ : β
⊢ a✝ ∈ pimage f ∅ ↔ a✝ ∈ ∅

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α →. β
inst✝ : (x : α) → Decidable (f x).Dom
⊢ pimage f ∅ = ∅

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq β
f : α →. β
inst✝ : (x : α) → Decidable (f x).Dom
a✝ : β
⊢ a✝ ∈ pimage f ∅ ↔ a✝ ∈ ∅
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive add_nsmul]
lemma pow_add (a : M) (m : ℕ) : ∀ n, a ^ (m + n) = a ^ m * a ^ n
  | 0 => by rw [Nat.add_zero, pow_zero, mul_one]
  | n + 1 => by rw [pow_succ, ← mul_assoc, ← pow_add, ← pow_succ, Nat.add_assoc]

Proof state:
M : Type u_2
inst✝ : Monoid M
a : M
m : ℕ
⊢ a ^ (m + 0) = a ^ m * a ^ 0

Tactic:
rw [Nat.add_zero, pow_zero, mul_one]

Result:
no goals

Proof state:
M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ (m + (n + 1)) = a ^ m * a ^ (n + 1)

Tactic:
rw [pow_succ, ← mul_assoc, ← pow_add, ← pow_succ, Nat.add_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (l H) :
    map g (pmap f l H) = pmap (fun a h => g (f a h)) l H

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
g : β → γ
f : (a : α) → p a → β
H : ∀ (a : α), a ∈ [] → p a
⊢ map g (pmap f [] H) = pmap (fun a h => g (f a h)) [] H

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
g : β → γ
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
⊢ map g (pmap f l H) = pmap (fun a h => g (f a h)) l H

Tactic:
induction l

Result:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
g : β → γ
f : (a : α) → p a → β
H : ∀ (a : α), a ∈ [] → p a
⊢ map g (pmap f [] H) = pmap (fun a h => g (f a h)) [] H

case cons
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
g : β → γ
f : (a : α) → p a → β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (H : ∀ (a : α), a ∈ tail✝ → p a), map g (pmap f tail✝ H) = pmap (fun a h => g (f a h)) tail✝ H
H : ∀ (a : α), a ∈ head✝ :: tail✝ → p a
⊢ map g (pmap f (head✝ :: tail✝) H) = pmap (fun a h => g (f a h)) (head✝ :: tail✝) H

Proof state:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
g : β → γ
f : (a : α) → p a → β
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (H : ∀ (a : α), a ∈ tail✝ → p a), map g (pmap f tail✝ H) = pmap (fun a h => g (f a h)) tail✝ H
H : ∀ (a : α), a ∈ head✝ :: tail✝ → p a
⊢ map g (pmap f (head✝ :: tail✝) H) = pmap (fun a h => g (f a h)) (head✝ :: tail✝) H

Tactic:
simp only [*, pmap, map]

Result:
no goals
-- Mathlib/Analysis/Convex/Basic.lean
theorem DirectedOn.convex_sUnion {c : Set (Set E)} (hdir : DirectedOn (· ⊆ ·) c)
    (hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A) : Convex 𝕜 (⋃₀ c)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
c : Set (Set E)
hdir : DirectedOn (fun x1 x2 => x1 ⊆ x2) c
hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A
⊢ Convex 𝕜 (⋃ i, ↑i)

Tactic:
exact (directedOn_iff_directed.1 hdir).convex_iUnion fun A => hc A.2

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
c : Set (Set E)
hdir : DirectedOn (fun x1 x2 => x1 ⊆ x2) c
hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A
⊢ Convex 𝕜 (⋃₀ c)

Tactic:
rw [sUnion_eq_iUnion]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
c : Set (Set E)
hdir : DirectedOn (fun x1 x2 => x1 ⊆ x2) c
hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A
⊢ Convex 𝕜 (⋃ i, ↑i)
-- Mathlib/Topology/Maps/Basic.lean
lemma Topology.IsInducing.isClosedMap (hf : IsInducing f) (h : IsClosed (range f)) :
    IsClosedMap f

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsInducing f
h : IsClosed (range f)
⊢ IsClosedMap f

Tactic:
intro s hs

Result:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsInducing f
h : IsClosed (range f)
s : Set X
hs : IsClosed s
⊢ IsClosed (f '' s)

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsInducing f
h : IsClosed (range f)
t : Set Y
ht : IsClosed t
hs : IsClosed (f ⁻¹' t)
⊢ IsClosed (t ∩ range f)

Tactic:
exact ht.inter h

Result:
no goals

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsInducing f
h : IsClosed (range f)
t : Set Y
ht : IsClosed t
hs : IsClosed (f ⁻¹' t)
⊢ IsClosed (f '' (f ⁻¹' t))

Tactic:
rw [image_preimage_eq_inter_range]

Result:
case intro.intro
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsInducing f
h : IsClosed (range f)
t : Set Y
ht : IsClosed t
hs : IsClosed (f ⁻¹' t)
⊢ IsClosed (t ∩ range f)

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsInducing f
h : IsClosed (range f)
s : Set X
hs : IsClosed s
⊢ IsClosed (f '' s)

Tactic:
rcases hf.isClosed_iff.1 hs with ⟨t, ht, rfl⟩

Result:
case intro.intro
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsInducing f
h : IsClosed (range f)
t : Set Y
ht : IsClosed t
hs : IsClosed (f ⁻¹' t)
⊢ IsClosed (f '' (f ⁻¹' t))
-- Mathlib/Order/PartialSups.lean
theorem partialSups_eq_biSup (f : ι → α) (i : ι) :
    partialSups f i = ⨆ j ≤ i, f j

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CompleteLattice α
f : ι → α
i : ι
⊢ (partialSups f) i = ⨆ j, ⨆ (_ : j ≤ i), f j

Tactic:
simpa only [iSup_subtype] using partialSups_eq_ciSup_Iic f i

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
/-- See also `Finset.prod_ite_eq'`. -/
@[to_additive "See also `Finset.sum_ite_eq'`."]
lemma prod_ite_eq' (i : ι) (f : ι → α) : ∏ j, (if j = i then f j else 1) = f i

Proof state:
ι : Type u_6
α : Type u_8
inst✝² : Fintype ι
inst✝¹ : CommMonoid α
inst✝ : DecidableEq ι
i : ι
f : ι → α
⊢ (∏ j : ι, if j = i then f j else 1) = f i

Tactic:
rw [Finset.prod_ite_eq', if_pos (mem_univ _)]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/WF.lean
theorem ndrecOn_eq_ndrecOnC : @Acc.ndrecOn = @Acc.ndrecOnC

Proof state:
⊢ @ndrecOn = @Acc.ndrecOnC

Tactic:
funext α r motive intro a t

Result:
case h.h.h.h.h.h
α : Sort u_1
r : α → α → Prop
motive : α → Sort u_2
intro : α
a : Acc r intro
t : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → motive y) → motive x
⊢ a.ndrecOn t = Acc.ndrecOnC a t

Proof state:
case h.h.h.h.h.h
α : Sort u_1
r : α → α → Prop
motive : α → Sort u_2
intro : α
a : Acc r intro
t : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → motive y) → motive x
⊢ a.ndrecOn t = Acc.ndrecOnC a t

Tactic:
rw [Acc.ndrecOn, rec_eq_recC, Acc.ndrecOnC]

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
lemma zero_mem_spectrum_inr (R S : Type*) {A : Type*} [CommSemiring R]
    [CommRing S] [Nontrivial S] [NonUnitalRing A] [Algebra R S] [Module S A] [IsScalarTower S A A]
    [SMulCommClass S A A] [Module R A] [IsScalarTower R S A] (a : A) :
    0 ∈ spectrum R (a : Unitization S A)

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁹ : CommSemiring R
inst✝⁸ : CommRing S
inst✝⁷ : Nontrivial S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ 0 ∈ spectrum R ↑a

Tactic:
rw [spectrum.zero_mem_iff]

Result:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁹ : CommSemiring R
inst✝⁸ : CommRing S
inst✝⁷ : Nontrivial S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ ¬IsUnit ↑a

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁹ : CommSemiring R
inst✝⁸ : CommRing S
inst✝⁷ : Nontrivial S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
⊢ ¬IsUnit ↑a

Tactic:
rintro ⟨u, hu⟩

Result:
case intro
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁹ : CommSemiring R
inst✝⁸ : CommRing S
inst✝⁷ : Nontrivial S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
u : (Unitization S A)ˣ
hu : ↑u = ↑a
⊢ False

Proof state:
case intro
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁹ : CommSemiring R
inst✝⁸ : CommRing S
inst✝⁷ : Nontrivial S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
u : (Unitization S A)ˣ
hu : ↑u = ↑a
⊢ False

Tactic:
simpa [-Units.mul_inv, hu] using congr($(u.mul_inv).fst)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Types.lean
@[ext]
lemma limitCone_pt_ext {x y : (limitCone F).pt}
    (w : (equivShrink F.sections).symm x = (equivShrink F.sections).symm y) : x = y

Proof state:
J : Type v
inst✝¹ : Category.{w, v} J
F : J ⥤ Type u
inst✝ : Small.{u, max u v} ↑F.sections
x y : (limitCone F).pt
w : (equivShrink ↑F.sections).symm x = (equivShrink ↑F.sections).symm y
⊢ x = y

Tactic:
aesop

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Basic.lean
theorem snoc_smul (f : MultilinearMap R M M₂) (m : ∀ i : Fin n, M (castSucc i)) (c : R)
    (x : M (last n)) : f (snoc m (c • x)) = c • f (snoc m x)

Proof state:
R : Type uR
n : ℕ
M : Fin n.succ → Type v
M₂ : Type v₂
inst✝⁴ : Semiring R
inst✝³ : (i : Fin n.succ) → AddCommMonoid (M i)
inst✝² : AddCommMonoid M₂
inst✝¹ : (i : Fin n.succ) → Module R (M i)
inst✝ : Module R M₂
f : MultilinearMap R M M₂
m : (i : Fin n) → M i.castSucc
c : R
x : M (last n)
⊢ f (snoc m (c • x)) = c • f (snoc m x)

Tactic:
simp_rw [← update_snoc_last x m (c • x), f.map_update_smul, update_snoc_last]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Grp_.lean
theorem lift_comp_inv_left {A : C} {B : Grp_ C} (f : A ⟶ B.X) :
    lift (f ≫ B.inv) f ≫ B.mul = toUnit _ ≫ B.one

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Grp_ C
f : A ⟶ B.X
⊢ lift (f ≫ B.inv) f ≫ B.mul = toUnit A ≫ B.one

Tactic:
have := f ≫= B.left_inv

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Grp_ C
f : A ⟶ B.X
this : f ≫ lift B.inv (𝟙 B.X) ≫ B.mul = f ≫ toUnit B.X ≫ B.one
⊢ lift (f ≫ B.inv) f ≫ B.mul = toUnit A ≫ B.one

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Grp_ C
f : A ⟶ B.X
this : f ≫ lift B.inv (𝟙 B.X) ≫ B.mul = f ≫ toUnit B.X ≫ B.one
⊢ lift (f ≫ B.inv) f ≫ B.mul = toUnit A ≫ B.one

Tactic:
rwa [comp_lift_assoc, comp_id, reassoc_of% toUnit_unique (f ≫ toUnit B.X) (toUnit A)] at this

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/UnitPartition.lean
theorem tag_injective : Function.Injective (fun ν : ι → ℤ ↦ tag n ν)

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
⊢ Function.Injective fun ν => tag n ν

Tactic:
refine fun _ _ h ↦ funext_iff.mpr fun i ↦ ?_

Result:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : ι → ℤ
h : (fun ν => tag n ν) x✝¹ = (fun ν => tag n ν) x✝
i : ι
⊢ x✝¹ i = x✝ i

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : ι → ℤ
h : (fun ν => tag n ν) x✝¹ = (fun ν => tag n ν) x✝
i : ι
this : x✝¹ i = x✝ i
⊢ x✝¹ i = x✝ i

Tactic:
exact this

Result:
no goals

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : ι → ℤ
h : (fun ν => tag n ν) x✝¹ = (fun ν => tag n ν) x✝
i : ι
this : (fun x => x i) ((fun ν => tag n ν) x✝¹) = (fun x => x i) ((fun ν => tag n ν) x✝)
⊢ x✝¹ i = x✝ i

Tactic:
simp_rw [tag_apply, div_left_inj' (c := (n : ℝ)) (Nat.cast_ne_zero.mpr (NeZero.ne n)),
  add_left_inj, Int.cast_inj] at this

Result:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : ι → ℤ
h : (fun ν => tag n ν) x✝¹ = (fun ν => tag n ν) x✝
i : ι
this : x✝¹ i = x✝ i
⊢ x✝¹ i = x✝ i

Proof state:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : ι → ℤ
h : (fun ν => tag n ν) x✝¹ = (fun ν => tag n ν) x✝
i : ι
⊢ x✝¹ i = x✝ i

Tactic:
have := congr_arg (fun x ↦ x i) h

Result:
ι : Type u_1
n : ℕ
inst✝ : NeZero n
x✝¹ x✝ : ι → ℤ
h : (fun ν => tag n ν) x✝¹ = (fun ν => tag n ν) x✝
i : ι
this : (fun x => x i) ((fun ν => tag n ν) x✝¹) = (fun x => x i) ((fun ν => tag n ν) x✝)
⊢ x✝¹ i = x✝ i