harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiag'_diagonal [DecidableEq o] [∀ i, DecidableEq (m' i)] (d : (Σi, m' i) → α) (k : o) :
    blockDiag' (diagonal d) k = diagonal fun i => d ⟨k, i⟩ :=
  ext fun i j => by
    obtain rfl | hij := Decidable.eq_or_ne i j
    · rw [blockDiag'_apply, diagonal_apply_eq, diagonal_apply_eq]
    · rw [blockDiag'_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt (fun h => ?_) hij)]
      cases h
      rfl

Proof state:
case inl
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
⊢ (diagonal d).blockDiag' k i i = diagonal (fun i => d ⟨k, i⟩) i i

Tactic:
rw [blockDiag'_apply, diagonal_apply_eq, diagonal_apply_eq]

Result:
no goals

Proof state:
case inr
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
⊢ (diagonal d).blockDiag' k i j = diagonal (fun i => d ⟨k, i⟩) i j

Tactic:
rw [blockDiag'_apply, diagonal_apply_ne _ hij, diagonal_apply_ne _ (mt (fun h => ?_) hij)]

Result:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
h : ⟨k, i⟩ = ⟨k, j⟩
⊢ i = j

Proof state:
case refl
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
hij : i ≠ i
⊢ i = i

Tactic:
rfl

Result:
no goals

Proof state:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
h : ⟨k, i⟩ = ⟨k, j⟩
⊢ i = j

Tactic:
cases h

Result:
case refl
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
hij : i ≠ i
⊢ i = i

Proof state:
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
⊢ (diagonal d).blockDiag' k i j = diagonal (fun i => d ⟨k, i⟩) i j

Tactic:
obtain rfl | hij := Decidable.eq_or_ne i j

Result:
case inl
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i : m' k
⊢ (diagonal d).blockDiag' k i i = diagonal (fun i => d ⟨k, i⟩) i i

case inr
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
⊢ (diagonal d).blockDiag' k i j = diagonal (fun i => d ⟨k, i⟩) i j
-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
lemma le_comap_range_lTensor (q : Q) :
    LinearMap.range g ≤ (LinearMap.range (lTensor Q g)).comap (TensorProduct.mk R Q P q)

Proof state:
case intro
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
q : Q
n : N
⊢ g n ∈ Submodule.comap ((TensorProduct.mk R Q P) q) (range (lTensor Q g))

Tactic:
exact ⟨q ⊗ₜ[R] n, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
q : Q
⊢ range g ≤ Submodule.comap ((TensorProduct.mk R Q P) q) (range (lTensor Q g))

Tactic:
rintro x ⟨n, rfl⟩

Result:
case intro
R : Type u_1
inst✝⁶ : CommSemiring R
N : Type u_3
P : Type u_4
Q : Type u_5
inst✝⁵ : AddCommMonoid N
inst✝⁴ : AddCommMonoid P
inst✝³ : AddCommMonoid Q
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
g : N →ₗ[R] P
q : Q
n : N
⊢ g n ∈ Submodule.comap ((TensorProduct.mk R Q P) q) (range (lTensor Q g))
-- Mathlib/Data/Sym/Sym2.lean
theorem other_ne {a : α} {z : Sym2 α} (hd : ¬IsDiag z) (h : a ∈ z) : Mem.other h ≠ a

Proof state:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : s(a, Mem.other h) = z
⊢ z.IsDiag

Tactic:
rw [hd] at h'

Result:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : s(a, a) = z
⊢ z.IsDiag

Proof state:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : s(a, a) = z
⊢ s(a, a).IsDiag

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : s(a, a) = z
⊢ z.IsDiag

Tactic:
rw [← h']

Result:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : s(a, a) = z
⊢ s(a, a).IsDiag

Proof state:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
⊢ z.IsDiag

Tactic:
have h' := Sym2.other_spec h

Result:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
h' : s(a, Mem.other h) = z
⊢ z.IsDiag

Proof state:
α : Type u_1
a : α
z : Sym2 α
hd : ¬z.IsDiag
h : a ∈ z
⊢ Mem.other h ≠ a

Tactic:
contrapose! hd

Result:
α : Type u_1
a : α
z : Sym2 α
h : a ∈ z
hd : Mem.other h = a
⊢ z.IsDiag
-- Mathlib/Computability/TMConfig.lean
theorem pred_eval (v) : pred.eval v = pure [v.headI.pred]

Proof state:
v : List ℕ
⊢ pred.eval v = pure [v.headI.pred]

Tactic:
simp [pred]

Result:
v : List ℕ
⊢ Nat.rec (Part.some [0]) (fun y x => Part.some [y]) v.headI = Part.some [v.headI - 1]

Proof state:
v : List ℕ
⊢ Nat.rec (Part.some [0]) (fun y x => Part.some [y]) v.headI = Part.some [v.headI - 1]

Tactic:
cases v.headI <;> simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma IsCycle.isPath_takeUntil {c : G.Walk v v} (hc : c.IsCycle) (h : w ∈ c.support) :
    (c.takeUntil w h).IsPath

Proof state:
case neg
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
h : w ∈ c.support
hc : ((c.dropUntil w h).reverse.append (c.takeUntil w h).reverse).IsCycle
hvw : ¬v = w
⊢ (c.takeUntil w h).IsPath

Tactic:
exact (c.takeUntil w h).isPath_reverse_iff.mp (hc.isPath_of_append_right (not_nil_of_ne hvw))

Result:
no goals

Proof state:
case neg
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
hvw : ¬v = w
⊢ (c.takeUntil w h).IsPath

Tactic:
rw [← isCycle_reverse, ← take_spec c h, reverse_append] at hc

Result:
case neg
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
h : w ∈ c.support
hc : ((c.dropUntil w h).reverse.append (c.takeUntil w h).reverse).IsCycle
hvw : ¬v = w
⊢ (c.takeUntil w h).IsPath

Proof state:
case pos
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : v ∈ c.support
⊢ (c.takeUntil v h).IsPath

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
⊢ (c.takeUntil w h).IsPath

Tactic:
by_cases hvw : v = w

Result:
case pos
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
hvw : v = w
⊢ (c.takeUntil w h).IsPath

case neg
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
hvw : ¬v = w
⊢ (c.takeUntil w h).IsPath

Proof state:
case pos
V : Type u
G : SimpleGraph V
v w : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : w ∈ c.support
hvw : v = w
⊢ (c.takeUntil w h).IsPath

Tactic:
subst hvw

Result:
case pos
V : Type u
G : SimpleGraph V
v : V
inst✝ : DecidableEq V
c : G.Walk v v
hc : c.IsCycle
h : v ∈ c.support
⊢ (c.takeUntil v h).IsPath
-- Mathlib/Data/Matroid/Map.lean
@[simp] lemma mapEquiv_isBase_iff {B : Set β} :
    (M.mapEquiv f).IsBase B ↔ M.IsBase (f.symm '' B)

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
B : Set β
h : M.IsBase (⇑f.symm '' B)
⊢ B = ⇑f '' (⇑f.symm '' B)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
B : Set β
⊢ (M.mapEquiv f).IsBase B ↔ M.IsBase (⇑f.symm '' B)

Tactic:
rw [mapEquiv_eq_map, map_isBase_iff]

Result:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
B : Set β
⊢ (∃ B₀, M.IsBase B₀ ∧ B = ⇑f '' B₀) ↔ M.IsBase (⇑f.symm '' B)

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
B : Set β
⊢ (∃ B₀, M.IsBase B₀ ∧ B = ⇑f '' B₀) ↔ M.IsBase (⇑f.symm '' B)

Tactic:
exact ⟨by rintro ⟨I, hI, rfl⟩; simpa, fun h ↦ ⟨_, h, by simp⟩⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set α
hI : M.IsBase I
⊢ M.IsBase (⇑f.symm '' (⇑f '' I))

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
B : Set β
⊢ (∃ B₀, M.IsBase B₀ ∧ B = ⇑f '' B₀) → M.IsBase (⇑f.symm '' B)

Tactic:
rintro ⟨I, hI, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
M : Matroid α
f : α ≃ β
I : Set α
hI : M.IsBase I
⊢ M.IsBase (⇑f.symm '' (⇑f '' I))
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem geom_series_succ (x : R) (h : ‖x‖ < 1) : ∑' i : ℕ, x ^ (i + 1) = ∑' i : ℕ, x ^ i - 1

Proof state:
R : Type u_2
inst✝¹ : NormedRing R
inst✝ : HasSummableGeomSeries R
x : R
h : ‖x‖ < 1
⊢ ∑' (i : ℕ), x ^ (i + 1) = ∑' (i : ℕ), x ^ i - 1

Tactic:
rw [eq_sub_iff_add_eq, tsum_eq_zero_add (summable_geometric_of_norm_lt_one h),
  pow_zero, add_comm]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Group.lean
theorem comap_abs_atTop : comap (abs : α → α) atTop = atBot ⊔ atTop

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
⊢ comap abs atTop = atBot ⊔ atTop

Tactic:
refine
  le_antisymm (((atTop_basis.comap _).le_basis_iff (atBot_basis.sup atTop_basis)).2 ?_)
    (sup_le tendsto_abs_atBot_atTop.le_comap tendsto_abs_atTop_atTop.le_comap)

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
⊢ ∀ (i' : α × α), True ∧ True → ∃ i, True ∧ abs ⁻¹' Ici i ⊆ Iic i'.1 ∪ Ici i'.2

Proof state:
case mk
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ ∃ i, True ∧ abs ⁻¹' Ici i ⊆ Iic (a, b).1 ∪ Ici (a, b).2

Tactic:
refine ⟨max (-a) b, trivial, fun x hx => ?_⟩

Result:
case mk
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b x : α
hx : x ∈ abs ⁻¹' Ici (-a ⊔ b)
⊢ x ∈ Iic (a, b).1 ∪ Ici (a, b).2

Proof state:
case mk
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b x : α
hx : x ≤ a ∧ x ≤ -b ∨ -a ≤ x ∧ b ≤ x
⊢ x ∈ Iic (a, b).1 ∪ Ici (a, b).2

Tactic:
exact hx.imp And.left And.right

Result:
no goals

Proof state:
case mk
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b x : α
hx : x ∈ abs ⁻¹' Ici (-a ⊔ b)
⊢ x ∈ Iic (a, b).1 ∪ Ici (a, b).2

Tactic:
rw [mem_preimage, mem_Ici, le_abs', max_le_iff, ← min_neg_neg, le_min_iff, neg_neg] at hx

Result:
case mk
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b x : α
hx : x ≤ a ∧ x ≤ -b ∨ -a ≤ x ∧ b ≤ x
⊢ x ∈ Iic (a, b).1 ∪ Ici (a, b).2

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
⊢ ∀ (i' : α × α), True ∧ True → ∃ i, True ∧ abs ⁻¹' Ici i ⊆ Iic i'.1 ∪ Ici i'.2

Tactic:
rintro ⟨a, b⟩ -

Result:
case mk
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b : α
⊢ ∃ i, True ∧ abs ⁻¹' Ici i ⊆ Iic (a, b).1 ∪ Ici (a, b).2
-- Mathlib/Probability/Kernel/Basic.lean
theorem setLIntegral_deterministic {f : β → ℝ≥0∞} {g : α → β} {a : α} (hg : Measurable g)
    [MeasurableSingletonClass β] (s : Set β) [Decidable (g a ∈ s)] :
    ∫⁻ x in s, f x ∂deterministic g hg a = if g a ∈ s then f (g a) else 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : β → ℝ≥0∞
g : α → β
a : α
hg : Measurable g
inst✝¹ : MeasurableSingletonClass β
s : Set β
inst✝ : Decidable (g a ∈ s)
⊢ ∫⁻ (x : β) in s, f x ∂(deterministic g hg) a = if g a ∈ s then f (g a) else 0

Tactic:
rw [deterministic_apply, setLIntegral_dirac f s]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem mem_sInf_iff : a ∈ sInf S ↔ ∃ s ∈ S, a ∈ s :=
  mem_iUnion₂.trans <| by simp only [exists_prop, SetLike.mem_coe]

Proof state:
α : Type u_1
inst✝ : LE α
S : Set (UpperSet α)
a : α
⊢ (∃ i, ∃ (_ : i ∈ S), a ∈ ↑i) ↔ ∃ s ∈ S, a ∈ s

Tactic:
simp only [exists_prop, SetLike.mem_coe]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma isGreatest_nnnorm_quasispectrum (a : A) (ha : p a

Proof state:
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
a : A
ha : autoParam (p a) _auto✝
⊢ IsGreatest ((fun x => ‖x‖₊) '' σₙ 𝕜 a) ‖a‖₊

Tactic:
simpa only [cfcₙ_id 𝕜 a] using IsGreatest.nnnorm_cfcₙ (id : 𝕜 → 𝕜) a

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem Submodule.finrank_eq_zero [StrongRankCondition R] [NoZeroSMulDivisors R M]
    {S : Submodule R M} [Module.Finite R S] :
    finrank R S = 0 ↔ S = ⊥

Proof state:
R : Type u
M : Type v
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
inst✝¹ : NoZeroSMulDivisors R M
S : Submodule R M
inst✝ : Module.Finite R ↥S
⊢ finrank R ↥S = 0 ↔ S = ⊥

Tactic:
rw [← Submodule.rank_eq_zero, ← finrank_eq_rank, ← @Nat.cast_zero Cardinal, Nat.cast_inj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Compare.lean
theorem compare_swap (a b : Nat) : (compare a b).swap = compare b a

Proof state:
a b : Nat
⊢ (if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt).swap =
    if b ≤ a then if a ≤ b then Ordering.eq else Ordering.lt else Ordering.gt

Tactic:
repeat' split

Result:
case isTrue.isTrue
a b : Nat
h✝¹ : a ≤ b
h✝ : b ≤ a
⊢ Ordering.eq.swap = Ordering.eq

case isTrue.isFalse
a b : Nat
h✝¹ : a ≤ b
h✝ : ¬b ≤ a
⊢ Ordering.lt.swap = Ordering.gt

case isFalse.isTrue
a b : Nat
h✝¹ : ¬a ≤ b
h✝ : b ≤ a
⊢ Ordering.gt.swap = Ordering.lt

case isFalse.isFalse
a b : Nat
h✝¹ : ¬a ≤ b
h✝ : ¬b ≤ a
⊢ Ordering.gt.swap = Ordering.gt

Proof state:
a b : Nat
⊢ (if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt).swap =
    if b ≤ a then if a ≤ b then Ordering.eq else Ordering.lt else Ordering.gt

Tactic:
(repeat' split) <;> try rfl

Result:
case isFalse.isFalse
a b : Nat
h✝¹ : ¬a ≤ b
h✝ : ¬b ≤ a
⊢ Ordering.gt.swap = Ordering.gt

Proof state:
case isFalse.isFalse
a b : Nat
h✝¹ : ¬a ≤ b
h✝ : ¬b ≤ a
⊢ Ordering.gt.swap = Ordering.gt

Tactic:
next h1 h2 => cases h1 (Nat.le_of_not_le h2)

Result:
no goals

Proof state:
a b : Nat
⊢ (compare a b).swap = compare b a

Tactic:
simp only [compare_def_le]

Result:
a b : Nat
⊢ (if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt).swap =
    if b ≤ a then if a ≤ b then Ordering.eq else Ordering.lt else Ordering.gt

Proof state:
case isFalse.isTrue
a b : Nat
h✝¹ : ¬a ≤ b
h✝ : b ≤ a
⊢ Ordering.gt.swap = Ordering.lt

Tactic:
rfl

Result:
no goals

Proof state:
case isFalse
a b : Nat
h✝ : ¬a ≤ b
⊢ Ordering.gt.swap = if b ≤ a then Ordering.lt else Ordering.gt

Tactic:
split

Result:
case isFalse.isTrue
a b : Nat
h✝¹ : ¬a ≤ b
h✝ : b ≤ a
⊢ Ordering.gt.swap = Ordering.lt

case isFalse.isFalse
a b : Nat
h✝¹ : ¬a ≤ b
h✝ : ¬b ≤ a
⊢ Ordering.gt.swap = Ordering.gt

Proof state:
a b : Nat
h1 : ¬a ≤ b
h2 : ¬b ≤ a
⊢ Ordering.gt.swap = Ordering.gt

Tactic:
cases h1 (Nat.le_of_not_le h2)

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem leadingCoeff_sub_of_lt {f g : MvPolynomial σ R} (h : m.degree g ≺[m] m.degree f) :
    m.leadingCoeff (f - g) = m.leadingCoeff f

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.leadingCoeff (f - g) = m.leadingCoeff f

Tactic:
rw [sub_eq_add_neg]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.leadingCoeff (f + -g) = m.leadingCoeff f

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.leadingCoeff (f + -g) = m.leadingCoeff f

Tactic:
apply leadingCoeff_add_of_lt

Result:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (-g)) < m.toSyn (m.degree f)

Proof state:
case h
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
h : m.toSyn (m.degree g) < m.toSyn (m.degree f)
⊢ m.toSyn (m.degree (-g)) < m.toSyn (m.degree f)

Tactic:
simp only [degree_neg, h]

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem rightCoset_assoc (s : Set α) (a b : α) : op b • op a • s = op (a * b) • s

Proof state:
α : Type u_1
inst✝ : Semigroup α
s : Set α
a b : α
⊢ op b • op a • s = op (a * b) • s

Tactic:
simp [← image_smul, (image_comp _ _ _).symm, Function.comp, mul_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurable_const' {f : β → α} (hf : ∀ x y, f x = f y) : Measurable f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : ∀ (x y : β), f x = f y
⊢ Measurable f

Tactic:
nontriviality β

Result:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : ∀ (x y : β), f x = f y
a✝ : Nontrivial β
⊢ Measurable f

Proof state:
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : ∀ (x y : β), f x = f y
a✝ : Nontrivial β
inhabited_h : Inhabited β
x✝ : β
⊢ f x✝ = f default

Tactic:
apply hf

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : ∀ (x y : β), f x = f y
a✝ : Nontrivial β
⊢ Measurable f

Tactic:
inhabit β

Result:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : ∀ (x y : β), f x = f y
a✝ : Nontrivial β
inhabited_h : Inhabited β
⊢ Measurable f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : ∀ (x y : β), f x = f y
a✝ : Nontrivial β
inhabited_h : Inhabited β
⊢ Measurable f

Tactic:
convert @measurable_const α β _ _ (f default) using 2

Result:
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
f : β → α
hf : ∀ (x y : β), f x = f y
a✝ : Nontrivial β
inhabited_h : Inhabited β
x✝ : β
⊢ f x✝ = f default
-- Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean
lemma inner_toCLM_conjTranspose_left {M : CStarMatrix m n A} {v : C⋆ᵐᵒᵈ (m → A)}
    {w : C⋆ᵐᵒᵈ (n → A)} : ⟪toCLM Mᴴ v, w⟫_A = ⟪v, toCLM M w⟫_A

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (m → A)
w : C⋆ᵐᵒᵈ (n → A)
⊢ ∑ x : n, ∑ i : m, star (v i) * M i x * w x = ∑ x : m, ∑ i : n, star (v x) * (M x i * w i)

Tactic:
rw [Finset.sum_comm]

Result:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (m → A)
w : C⋆ᵐᵒᵈ (n → A)
⊢ ∑ y : m, ∑ x : n, star (v y) * M y x * w x = ∑ x : m, ∑ i : n, star (v x) * (M x i * w i)

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (m → A)
w : C⋆ᵐᵒᵈ (n → A)
⊢ ⟪(toCLM Mᴴ) v, w⟫_A = ⟪v, (toCLM M) w⟫_A

Tactic:
simp only [toCLM_apply_eq_sum, pi_inner, equiv_symm_pi_apply, inner_def, Finset.mul_sum,
  Matrix.conjTranspose_apply, star_sum, star_mul, star_star, Finset.sum_mul]

Result:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (m → A)
w : C⋆ᵐᵒᵈ (n → A)
⊢ ∑ x : n, ∑ i : m, star (v i) * M i x * w x = ∑ x : m, ∑ i : n, star (v x) * (M x i * w i)

Proof state:
m : Type u_1
n : Type u_2
A : Type u_3
inst✝⁴ : Fintype n
inst✝³ : NonUnitalCStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Fintype m
M : CStarMatrix m n A
v : C⋆ᵐᵒᵈ (m → A)
w : C⋆ᵐᵒᵈ (n → A)
⊢ ∑ y : m, ∑ x : n, star (v y) * M y x * w x = ∑ x : m, ∑ i : n, star (v x) * (M x i * w i)

Tactic:
simp_rw [mul_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem inv_eq_of_hom_inv_id {f : X ⟶ Y} [IsIso f] {g : Y ⟶ X} (hom_inv_id : f ≫ g = 𝟙 X) :
    inv f = g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
g : Y ⟶ X
hom_inv_id : f ≫ g = 𝟙 X
⊢ inv f = g

Tactic:
apply (cancel_epi f).mp

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
g : Y ⟶ X
hom_inv_id : f ≫ g = 𝟙 X
⊢ f ≫ inv f = f ≫ g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
g : Y ⟶ X
hom_inv_id : f ≫ g = 𝟙 X
⊢ f ≫ inv f = f ≫ g

Tactic:
simp [hom_inv_id]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem div_lt_div_iff_right (c : α) : a / c < b / c ↔ a < b

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LT α
inst✝ : MulRightStrictMono α
a b c : α
⊢ a / c < b / c ↔ a < b

Tactic:
simpa only [div_eq_mul_inv] using mul_lt_mul_iff_right _

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
lemma antivary_iff_forall_smul_nonpos : Antivary f g ↔ ∀ i j, (f j - f i) • (g j - g i) ≤ 0 :=
monovary_toDual_right.symm.trans <| by rw [monovary_iff_forall_smul_nonneg]; rfl

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
f : ι → α
g : ι → β
⊢ Monovary f (⇑OrderDual.toDual ∘ g) ↔ ∀ (i j : ι), (f j - f i) • (g j - g i) ≤ 0

Tactic:
rw [monovary_iff_forall_smul_nonneg]

Result:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
f : ι → α
g : ι → β
⊢ (∀ (i j : ι), 0 ≤ (f j - f i) • ((⇑OrderDual.toDual ∘ g) j - (⇑OrderDual.toDual ∘ g) i)) ↔
    ∀ (i j : ι), (f j - f i) • (g j - g i) ≤ 0

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
f : ι → α
g : ι → β
⊢ (∀ (i j : ι), 0 ≤ (f j - f i) • ((⇑OrderDual.toDual ∘ g) j - (⇑OrderDual.toDual ∘ g) i)) ↔
    ∀ (i j : ι), (f j - f i) • (g j - g i) ≤ 0

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem take_add_one {l : List α} {n : Nat} :
    l.take (n + 1) = l.take n ++ l[n]?.toList

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ take (n + 1) l = take n l ++ l[n]?.toList

Tactic:
simp [take_add, take_one]

Result:
no goals
-- Mathlib/Topology/StoneCech.lean
theorem ultrafilterBasis_is_basis : TopologicalSpace.IsTopologicalBasis (ultrafilterBasis α) :=
  ⟨by
    rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ u ⟨ua, ub⟩
    refine ⟨_, ⟨a ∩ b, rfl⟩, inter_mem ua ub, fun v hv ↦ ⟨?_, ?_⟩⟩ <;> apply mem_of_superset hv <;>
      simp [inter_subset_right],
    eq_univ_of_univ_subset <| subset_sUnion_of_mem <| ⟨univ, eq_univ_of_forall fun _ ↦ univ_mem⟩,
    rfl⟩

Proof state:
α : Type u
⊢ ∀ t₁ ∈ ultrafilterBasis α, ∀ t₂ ∈ ultrafilterBasis α, ∀ x ∈ t₁ ∩ t₂, ∃ t₃ ∈ ultrafilterBasis α, x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂

Tactic:
rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩ u ⟨ua, ub⟩

Result:
case intro.intro.intro
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s => {u | s ∈ u}) a
ub : u ∈ (fun s => {u | s ∈ u}) b
⊢ ∃ t₃ ∈ ultrafilterBasis α, u ∈ t₃ ∧ t₃ ⊆ (fun s => {u | s ∈ u}) a ∩ (fun s => {u | s ∈ u}) b

Proof state:
case intro.intro.intro
α : Type u
a b : Set α
u : Ultrafilter α
ua : u ∈ (fun s => {u | s ∈ u}) a
ub : u ∈ (fun s => {u | s ∈ u}) b
⊢ ∃ t₃ ∈ ultrafilterBasis α, u ∈ t₃ ∧ t₃ ⊆ (fun s => {u | s ∈ u}) a ∩ (fun s => {u | s ∈ u}) b

Tactic:
refine ⟨_, ⟨a ∩ b, rfl⟩, inter_mem ua ub, fun v hv ↦ ⟨?_, ?_⟩⟩ <;> apply mem_of_superset hv <;>
  simp [inter_subset_right]

Result:
no goals
-- Mathlib/Order/Category/BddDistLat.lean
lemma id_apply (X : BddDistLat) (x : X) :
    (𝟙 X : X ⟶ X) x = x

Proof state:
X : BddDistLat
x : ↑X.toDistLat
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Result:
no goals