harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem adjugate_fin_two (A : Matrix (Fin 2) (Fin 2) α) :
    adjugate A = !![A 1 1, -A 0 1; -A 1 0, A 0 0]

Proof state:
case a
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ A.adjugate i j = !![A 1 1, -A 0 1; -A 1 0, A 0 0] i j

Tactic:
rw [adjugate_fin_succ_eq_det_submatrix]

Result:
case a
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det = !![A 1 1, -A 0 1; -A 1 0, A 0 0] i j

Proof state:
case a
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ (-1) ^ (↑j + ↑i) * (A.submatrix j.succAbove i.succAbove).det = !![A 1 1, -A 0 1; -A 1 0, A 0 0] i j

Tactic:
fin_cases i <;> fin_cases j <;> simp

Result:
no goals

Proof state:
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
⊢ A.adjugate = !![A 1 1, -A 0 1; -A 1 0, A 0 0]

Tactic:
ext i j

Result:
case a
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ A.adjugate i j = !![A 1 1, -A 0 1; -A 1 0, A 0 0] i j
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_eraseKey_of_beq [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α}
    (hl : DistinctKeys l) (hka : k == a) : getValue? a (eraseKey k l) = none

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × β)
k a : α
hl : DistinctKeys l
hka : (k == a) = true
⊢ getValue? a (eraseKey k l) = none

Tactic:
simp [getValue?_eq_getEntry?, getEntry?_eraseKey_of_beq hl hka]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem limit.pre_post {D : Type u'} [Category.{v'} D] (E : K ⥤ J) (F : J ⥤ C) (G : C ⥤ D)
    [HasLimit F] [HasLimit (E ⋙ F)] [HasLimit (F ⋙ G)]
    [h : HasLimit ((E ⋙ F) ⋙ G)] :-- G (limit F) ⟶ G (limit (E ⋙ F)) ⟶ limit ((E ⋙ F) ⋙ G) vs
            -- G (limit F) ⟶ limit F ⋙ G ⟶ limit (E ⋙ (F ⋙ G)) or
    haveI : HasLimit (E ⋙ F ⋙ G) := h
    G.map (limit.pre F E) ≫ limit.post (E ⋙ F) G = limit.post F G ≫ limit.pre (F ⋙ G) E

Proof state:
case w
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j✝ : K
⊢ (G.map (pre F E) ≫ post (E ⋙ F) G) ≫ π ((E ⋙ F) ⋙ G) j✝ = (post F G ≫ pre (F ⋙ G) E) ≫ π ((E ⋙ F) ⋙ G) j✝

Tactic:
erw [assoc, limit.post_π, ← G.map_comp, limit.pre_π, assoc, limit.pre_π, limit.post_π]

Result:
no goals

Proof state:
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
⊢ G.map (pre F E) ≫ post (E ⋙ F) G = post F G ≫ pre (F ⋙ G) E

Tactic:
ext

Result:
case w
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j✝ : K
⊢ (G.map (pre F E) ≫ post (E ⋙ F) G) ≫ π ((E ⋙ F) ⋙ G) j✝ = (post F G ≫ pre (F ⋙ G) E) ≫ π ((E ⋙ F) ⋙ G) j✝

Proof state:
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
⊢ G.map (pre F E) ≫ post (E ⋙ F) G = post F G ≫ pre (F ⋙ G) E

Tactic:
haveI : HasLimit (E ⋙ F ⋙ G) := h

Result:
J : Type u₁
inst✝⁶ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁵ : Category.{v₂, u₂} K
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
E : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
⊢ G.map (pre F E) ≫ post (E ⋙ F) G = post F G ≫ pre (F ⋙ G) E
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem MemLp.eLpNorm_mk_lt_top {α E : Type*} [MeasurableSpace α] {μ : Measure α}
    [NormedAddCommGroup E] {p : ℝ≥0∞} {f : α → E} (hfp : MemLp f p μ) :
    eLpNorm (AEEqFun.mk f hfp.1) p μ < ∞

Proof state:
α : Type u_7
E : Type u_8
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
f : α → E
hfp : MemLp f p μ
⊢ eLpNorm (↑(AEEqFun.mk f ⋯)) p μ < ⊤

Tactic:
simp [hfp.2]

Result:
no goals
-- Mathlib/LinearAlgebra/DFinsupp.lean
theorem mapRange_smul (f : ∀ i, β₁ i → β₂ i) (hf : ∀ i, f i 0 = 0) (r : R)
    (hf' : ∀ i x, f i (r • x) = r • f i x) (g : Π₀ i, β₁ i) :
    mapRange f hf (r • g) = r • mapRange f hf g

Proof state:
case h
ι : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
β₁ : ι → Type u_7
β₂ : ι → Type u_8
inst✝³ : (i : ι) → AddCommMonoid (β₁ i)
inst✝² : (i : ι) → AddCommMonoid (β₂ i)
inst✝¹ : (i : ι) → Module R (β₁ i)
inst✝ : (i : ι) → Module R (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
r : R
hf' : ∀ (i : ι) (x : β₁ i), f i (r • x) = r • f i x
g : Π₀ (i : ι), β₁ i
i✝ : ι
⊢ (mapRange f hf (r • g)) i✝ = (r • mapRange f hf g) i✝

Tactic:
simp only [mapRange_apply f, coe_smul, Pi.smul_apply, hf']

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
β₁ : ι → Type u_7
β₂ : ι → Type u_8
inst✝³ : (i : ι) → AddCommMonoid (β₁ i)
inst✝² : (i : ι) → AddCommMonoid (β₂ i)
inst✝¹ : (i : ι) → Module R (β₁ i)
inst✝ : (i : ι) → Module R (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
r : R
hf' : ∀ (i : ι) (x : β₁ i), f i (r • x) = r • f i x
g : Π₀ (i : ι), β₁ i
⊢ mapRange f hf (r • g) = r • mapRange f hf g

Tactic:
ext

Result:
case h
ι : Type u_1
R : Type u_2
inst✝⁴ : Semiring R
β₁ : ι → Type u_7
β₂ : ι → Type u_8
inst✝³ : (i : ι) → AddCommMonoid (β₁ i)
inst✝² : (i : ι) → AddCommMonoid (β₂ i)
inst✝¹ : (i : ι) → Module R (β₁ i)
inst✝ : (i : ι) → Module R (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
r : R
hf' : ∀ (i : ι) (x : β₁ i), f i (r • x) = r • f i x
g : Π₀ (i : ι), β₁ i
i✝ : ι
⊢ (mapRange f hf (r • g)) i✝ = (r • mapRange f hf g) i✝
-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
lemma lTensor.inverse_apply (y : Q ⊗[R] N) :
    (lTensor.inverse Q hfg hg) ((lTensor Q g) y) =
      Submodule.Quotient.mk (p := (LinearMap.range (lTensor Q f))) y

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : AddCommGroup N
inst✝⁵ : AddCommGroup P
inst✝⁴ : Module R M
inst✝³ : Module R N
inst✝² : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
hfg : Exact ⇑f ⇑g
hg : Surjective ⇑g
y : Q ⊗[R] N
⊢ (inverse Q hfg hg) ((lTensor Q g) y) = Submodule.Quotient.mk y

Tactic:
rw [lTensor.inverse, lTensor.inverse_of_rightInverse_apply]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Center.lean
@[simp] lemma div_mem_centralizer₀ (ha : a ∈ centralizer s) (hb : b ∈ centralizer s) :
    a / b ∈ centralizer s

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a b : G₀
ha : a ∈ s.centralizer
hb : b ∈ s.centralizer
⊢ a / b ∈ s.centralizer

Tactic:
simpa only [div_eq_mul_inv] using mul_mem_centralizer ha (inv_mem_centralizer₀ hb)

Result:
no goals
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem zpow : ∀ (n : ℤ) {w x}, c w x → c (w ^ n) (x ^ n)
  | Int.ofNat n, w, x, h => by simpa only [zpow_natCast, Int.ofNat_eq_coe] using c.pow n h
  | Int.negSucc n, w, x, h => by simpa only [zpow_negSucc] using c.inv (c.pow _ h)

Proof state:
M : Type u_1
inst✝ : Group M
c : Con M
n : ℕ
w x : M
h : c w x
⊢ c (w ^ Int.negSucc n) (x ^ Int.negSucc n)

Tactic:
simpa only [zpow_negSucc] using c.inv (c.pow _ h)

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Group M
c : Con M
n : ℕ
w x : M
h : c w x
⊢ c (w ^ Int.ofNat n) (x ^ Int.ofNat n)

Tactic:
simpa only [zpow_natCast, Int.ofNat_eq_coe] using c.pow n h

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem pow_bit1 {k : ℕ} {d : R} (_ : (a : R) ^ k = b) (_ : b * b = c) (_ : c * a = d) :
    a ^ (Nat.add (Nat.mul (nat_lit 2) k) (nat_lit 1)) = d

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a b c : R
k : ℕ
d : R
x✝² : a ^ k = b
x✝¹ : b * b = c
x✝ : c * a = d
⊢ a ^ (Nat.mul 2 k).add 1 = d

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a : R
k : ℕ
⊢ a ^ (Nat.mul 2 k).add 1 = a ^ k * a ^ k * a

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a : R
k : ℕ
⊢ a ^ (Nat.mul 2 k).add 1 = a ^ k * a ^ k * a

Tactic:
simp [Nat.succ_mul, pow_add]

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma le_of_forall_lt_iff_le : (∀ b : α, x < b → y ≤ b) ↔ y ≤ x

Proof state:
α : Type u_1
inst✝² : LinearOrder α
x y : WithTop α
inst✝¹ : DenselyOrdered α
inst✝ : NoMaxOrder α
⊢ (∀ (b : α), x < ↑b → y ≤ ↑b) ↔ y ≤ x

Tactic:
cases x <;> cases y <;> simp [exists_gt, forall_gt_imp_ge_iff_le_of_dense]

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem not_isPredPrelimit_of_noMin [NoMaxOrder α] : ¬ IsPredPrelimit a

Proof state:
α : Type u_1
a : α
inst✝⁴ : Preorder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
⊢ ¬IsPredPrelimit a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
lemma disjSum_eq_iff : s.disjSum t = u ↔ s = u.toLeft ∧ t = u.toRight :=
  ⟨fun h => by simp [← h], fun h => by simp [h, toLeft_disjSum_toRight]⟩

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
h : s.disjSum t = u
⊢ s = u.toLeft ∧ t = u.toRight

Tactic:
simp [← h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
u : Finset (α ⊕ β)
h : s = u.toLeft ∧ t = u.toRight
⊢ s.disjSum t = u

Tactic:
simp [h, toLeft_disjSum_toRight]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Degree.lean
theorem intDegree_mul {x y : RatFunc K} (hx : x ≠ 0) (hy : y ≠ 0) :
    intDegree (x * y) = intDegree x + intDegree y

Proof state:
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(x * y).num.natDegree + (↑x.denom.natDegree + ↑y.denom.natDegree) =
    ↑x.num.natDegree + ↑y.num.natDegree + ↑(x * y).denom.natDegree

Tactic:
norm_cast

Result:
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).num.natDegree + (x.denom.natDegree + y.denom.natDegree) =
    x.num.natDegree + y.num.natDegree + (x * y).denom.natDegree

Proof state:
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).num.natDegree + (x.denom.natDegree + y.denom.natDegree) =
    x.num.natDegree + y.num.natDegree + (x * y).denom.natDegree

Tactic:
rw [← Polynomial.natDegree_mul x.denom_ne_zero y.denom_ne_zero, ←
  Polynomial.natDegree_mul (RatFunc.num_ne_zero (mul_ne_zero hx hy))
    (mul_ne_zero x.denom_ne_zero y.denom_ne_zero),
  ← Polynomial.natDegree_mul (RatFunc.num_ne_zero hx) (RatFunc.num_ne_zero hy), ←
  Polynomial.natDegree_mul (mul_ne_zero (RatFunc.num_ne_zero hx) (RatFunc.num_ne_zero hy))
    (x * y).denom_ne_zero,
  RatFunc.num_denom_mul]

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).intDegree = x.intDegree + y.intDegree

Tactic:
simp only [intDegree, add_sub, sub_add, sub_sub_eq_add_sub, sub_sub, sub_eq_sub_iff_add_eq_add]

Result:
K : Type u
inst✝ : Field K
x y : RatFunc K
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(x * y).num.natDegree + (↑x.denom.natDegree + ↑y.denom.natDegree) =
    ↑x.num.natDegree + ↑y.num.natDegree + ↑(x * y).denom.natDegree
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem range_eq_univ (h : α ≃ᵢ β) : range h = univ

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
h : α ≃ᵢ β
⊢ range ⇑h = univ

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem quadratic_reciprocity {a b : ℕ} (ha : Odd a) (hb : Odd b) :
    J(a | b) = (-1) ^ (a / 2 * (b / 2)) * J(b | a)

Proof state:
a b : ℕ
ha : Odd a
hb : Odd b
⊢ J(↑a | b) = (-1) ^ (a / 2 * (b / 2)) * J(↑b | a)

Tactic:
rw [← qrSign.neg_one_pow ha hb, qrSign.symm ha hb, quadratic_reciprocity' ha hb]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem ediam_Icc (a b : ℝ) : EMetric.diam (Icc a b) = ENNReal.ofReal (b - a)

Proof state:
case inr
a b : ℝ
h : b < a
⊢ EMetric.diam (Icc a b) = ENNReal.ofReal (b - a)

Tactic:
simp [h, h.le]

Result:
no goals

Proof state:
case inl
a b : ℝ
h : a ≤ b
⊢ EMetric.diam (Icc a b) = ENNReal.ofReal (b - a)

Tactic:
rw [Real.ediam_eq (isBounded_Icc _ _), csSup_Icc h, csInf_Icc h]

Result:
no goals

Proof state:
a b : ℝ
⊢ EMetric.diam (Icc a b) = ENNReal.ofReal (b - a)

Tactic:
rcases le_or_lt a b with (h | h)

Result:
case inl
a b : ℝ
h : a ≤ b
⊢ EMetric.diam (Icc a b) = ENNReal.ofReal (b - a)

case inr
a b : ℝ
h : b < a
⊢ EMetric.diam (Icc a b) = ENNReal.ofReal (b - a)
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem support_update_ne_zero (p : R[X]) (n : ℕ) {a : R} (ha : a ≠ 0) :
    support (p.update n a) = insert n p.support

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
ha : a ≠ 0
⊢ (p.update n a).support = insert n p.support

Tactic:
rw [support_update, if_neg ha]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
a : R
ha : a ≠ 0
⊢ (p.update n a).support = insert n p.support

Tactic:
classical rw [support_update, if_neg ha]

Result:
no goals
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mpullback_eq_pullback {f : E → E'} {V : E' → E'} :
    mpullback 𝓘(𝕜, E) 𝓘(𝕜, E') f V = pullback 𝕜 f V

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
E' : Type u_6
inst✝¹ : NormedAddCommGroup E'
inst✝ : NormedSpace 𝕜 E'
f : E → E'
V : E' → E'
⊢ mpullback 𝓘(𝕜, E) 𝓘(𝕜, E') f V = pullback 𝕜 f V

Tactic:
simp only [← mpullbackWithin_univ, ← pullbackWithin_univ, mpullbackWithin_eq_pullbackWithin]

Result:
no goals
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem transcendental_algebraMap_iff {a : S} (h : Function.Injective (algebraMap S A)) :
    Transcendental R (algebraMap S A a) ↔ Transcendental R a

Proof state:
R : Type u
S : Type u_1
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
a : S
h : Function.Injective ⇑(algebraMap S A)
⊢ Transcendental R ((algebraMap S A) a) ↔ Transcendental R a

Tactic:
simp_rw [Transcendental, isAlgebraic_algebraMap_iff h]

Result:
no goals
-- Mathlib/Algebra/Group/Pi/Basic.lean
theorem apply_mulSingle (f' : ∀ i, f i → g i) (hf' : ∀ i, f' i 1 = 1) (i : I) (x : f i) (j : I) :
    f' j (mulSingle i x j) = mulSingle i (f' i x) j

Proof state:
I : Type u
f : I → Type v₁
g : I → Type v₂
inst✝² : DecidableEq I
inst✝¹ : (i : I) → One (f i)
inst✝ : (i : I) → One (g i)
f' : (i : I) → f i → g i
hf' : ∀ (i : I), f' i 1 = 1
i : I
x : f i
j : I
⊢ f' j (mulSingle i x j) = mulSingle i (f' i x) j

Tactic:
simpa only [Pi.one_apply, hf', mulSingle] using Function.apply_update f' 1 i x j

Result:
no goals
-- Mathlib/Topology/Order/UpperLowerSetTopology.lean
lemma isOpen_iff_isUpperSet : IsOpen s ↔ IsUpperSet s

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : Topology.IsUpperSet α
s : Set α
⊢ IsOpen s ↔ IsUpperSet s

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem one_div_le_one_div_of_neg (ha : a < 0) (hb : b < 0) : 1 / a ≤ 1 / b ↔ b ≤ a

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b : α
ha : a < 0
hb : b < 0
⊢ 1 / a ≤ 1 / b ↔ b ≤ a

Tactic:
simpa [one_div] using inv_le_inv_of_neg ha hb

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma bot_mul_of_pos {x : EReal} (h : 0 < x) : ⊥ * x = ⊥

Proof state:
x : EReal
h : 0 < x
⊢ ⊥ * x = ⊥

Tactic:
rw [EReal.mul_comm]

Result:
x : EReal
h : 0 < x
⊢ x * ⊥ = ⊥

Proof state:
x : EReal
h : 0 < x
⊢ x * ⊥ = ⊥

Tactic:
exact mul_bot_of_pos h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_insert [LawfulBEq α] (h : m.1.WF) {a k : α} {v : β k} : (m.insert k v).get? a =
    if h : k == a then some (cast (congrArg β (eq_of_beq h)) v) else m.get? a

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
a k : α
v : β k
⊢ (m.insert k v).get? a = if h : (k == a) = true then some (cast ⋯ v) else m.get? a

Tactic:
simp_to_model [insert] using List.getValueCast?_insertEntry

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degreeOf_C (a : R) (x : σ) : degreeOf x (C a : MvPolynomial σ R) = 0

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : R
x : σ
⊢ degreeOf x (C a) = 0

Tactic:
simp [degreeOf_def, degrees_C]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : R
x : σ
⊢ degreeOf x (C a) = 0

Tactic:
classical simp [degreeOf_def, degrees_C]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Datatypes.lean
theorem structuralIsoOfExpr_whiskerLeft (f : a ⟶ b) {g h : b ⟶ c}
    (η : g ⟶ h) (η' : g ≅ h) (ih_η : η'.hom = η)  :
    (whiskerLeftIso f η').hom = f ◁ η

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ⟶ h
η' : g ≅ h
ih_η : η'.hom = η
⊢ (whiskerLeftIso f η').hom = f ◁ η

Tactic:
simp [ih_η]

Result:
no goals
-- Mathlib/CategoryTheory/CommSq.lean
theorem iff_unop {A B X Y : Cᵒᵖ} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {g : B ⟶ Y}
    (sq : CommSq f i p g) : HasLift sq ↔ HasLift sq.unop

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ sq.HasLift ↔ ⋯.HasLift

Tactic:
rw [iff, iff]

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Nonempty sq.LiftStruct ↔ Nonempty ⋯.LiftStruct

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B X Y : Cᵒᵖ
f : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
g : B ⟶ Y
sq : CommSq f i p g
⊢ Nonempty sq.LiftStruct ↔ Nonempty ⋯.LiftStruct

Tactic:
exact Nonempty.congr (LiftStruct.unopEquiv sq).toFun (LiftStruct.unopEquiv sq).invFun

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_eq_zero_of_column_eq_zero {A : Matrix n n R} (j : n) (h : ∀ i, A i j = 0) :
    det A = 0

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
j : n
h : ∀ (i : n), A i j = 0
⊢ A.det = 0

Tactic:
rw [← det_transpose]

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
j : n
h : ∀ (i : n), A i j = 0
⊢ Aᵀ.det = 0

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
j : n
h : ∀ (i : n), A i j = 0
⊢ Aᵀ.det = 0

Tactic:
exact det_eq_zero_of_row_eq_zero j h

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/EventuallyMeasurable.lean
theorem EventuallyMeasurableSet.congr
    (ht : EventuallyMeasurableSet m l t) (hst : s =ᶠ[l] t) : EventuallyMeasurableSet m l s

Proof state:
α : Type u_1
m : MeasurableSpace α
s t : Set α
l : Filter α
inst✝ : CountableInterFilter l
ht : EventuallyMeasurableSet m l t
hst : s =ᶠ[l] t
⊢ EventuallyMeasurableSet m l s

Tactic:
rcases ht with ⟨t', ht', htt'⟩

Result:
case intro.intro
α : Type u_1
m : MeasurableSpace α
s t : Set α
l : Filter α
inst✝ : CountableInterFilter l
hst : s =ᶠ[l] t
t' : Set α
ht' : MeasurableSet t'
htt' : t =ᶠ[l] t'
⊢ EventuallyMeasurableSet m l s

Proof state:
case intro.intro
α : Type u_1
m : MeasurableSpace α
s t : Set α
l : Filter α
inst✝ : CountableInterFilter l
hst : s =ᶠ[l] t
t' : Set α
ht' : MeasurableSet t'
htt' : t =ᶠ[l] t'
⊢ EventuallyMeasurableSet m l s

Tactic:
exact ⟨t', ht', hst.trans htt'⟩

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem ofFractionRing_mk' (x : K[X]) (y : K[X]⁰) :
    ofFractionRing (IsLocalization.mk' _ x y) =
      IsLocalization.mk' (RatFunc K) x y

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x : K[X]
y : ↥K[X]⁰
⊢ { toFractionRing := IsLocalization.mk' (FractionRing K[X]) x y } = IsLocalization.mk' (RatFunc K) x y

Tactic:
rw [IsFractionRing.mk'_eq_div, IsFractionRing.mk'_eq_div, ← mk_eq_div', ← mk_eq_div]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Count.lean
theorem countP_false : (countP fun (_ : α) => false) = (fun (_ : Vector α n) => 0)

Proof state:
α : Type u_1
n : Nat
⊢ (countP fun x => false) = fun x => 0

Tactic:
funext l

Result:
case h
α : Type u_1
n : Nat
l : Vector α n
⊢ countP (fun x => false) l = 0

Proof state:
case h
α : Type u_1
n : Nat
l : Vector α n
⊢ countP (fun x => false) l = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
@[simp]
lemma neg_comp (α : Ext X Y n) {m : ℕ} (β : Ext Y Z m) {p : ℕ} (h : n + m = p) :
    (-α).comp β h = -α.comp β h

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
⊢ (-α).comp β h = -α.comp β h

Tactic:
letI := HasDerivedCategory.standard C

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (-α).comp β h = -α.comp β h

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ ((-α).comp β h).hom = (-α.comp β h).hom

Tactic:
simp [this, neg_hom']

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (-α).comp β h = -α.comp β h

Tactic:
ext

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ ((-α).comp β h).hom = (-α.comp β h).hom
-- Mathlib/Tactic/Module.lean
theorem eq_of_eval_eq_eval {R₁ R₂ : Type*} [AddCommMonoid M] [Semiring R] [Module R M] [Semiring R₁]
    [Module R₁ M] [Semiring R₂] [Module R₂ M]  {l₁ l₂ : NF R M} {l₁' : NF R₁ M} {l₂' : NF R₂ M}
    {x₁ x₂ : M} (hx₁ : x₁ = l₁'.eval) (hx₂ : x₂ = l₂'.eval) (h₁ : l₁.eval = l₁'.eval)
    (h₂ : l₂.eval = l₂'.eval) (h : l₁.eval = l₂.eval) :
    x₁ = x₂

Proof state:
R : Type u_2
M : Type u_3
R₁ : Type u_4
R₂ : Type u_5
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Semiring R
inst✝⁴ : Module R M
inst✝³ : Semiring R₁
inst✝² : Module R₁ M
inst✝¹ : Semiring R₂
inst✝ : Module R₂ M
l₁ l₂ : NF R M
l₁' : NF R₁ M
l₂' : NF R₂ M
x₁ x₂ : M
hx₁ : x₁ = l₁'.eval
hx₂ : x₂ = l₂'.eval
h₁ : l₁.eval = l₁'.eval
h₂ : l₂.eval = l₂'.eval
h : l₁.eval = l₂.eval
⊢ x₁ = x₂

Tactic:
rw [hx₁, hx₂, ← h₁, ← h₂, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_unitOfList_of_mem [EquivBEq α] [LawfulHashable α]
    [Inhabited α] {l : List α} {k k' : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a == b) = false))
    (mem : k ∈ l) :
    getKey! (unitOfList l) k' = k

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List α
k k' : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a == b) = false) l
mem : k ∈ l
⊢ (unitOfList l).getKey! k' = k

Tactic:
simp_to_raw using Raw₀.Const.getKey!_insertManyIfNewUnit_empty_list_of_mem

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem zero_smul_set {s : Set β} (h : s.Nonempty) : (0 : α) • s = (0 : Set β)

Proof state:
α : Type u_2
β : Type u_3
inst✝² : Zero α
inst✝¹ : Zero β
inst✝ : SMulWithZero α β
s : Set β
h : s.Nonempty
⊢ 0 • s = 0

Tactic:
simp only [← image_smul, image_eta, zero_smul, h.image_const, singleton_zero]

Result:
no goals