harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_eq_single (f : α → M) (a : α) (ha : ∀ x, x ≠ a → f x = 1) :
    ∏ᶠ x, f x = f a

Proof state:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
⊢ ∏ᶠ (x : α), f x = f a

Tactic:
have : mulSupport (f ∘ PLift.down) ⊆ ({PLift.up a} : Finset (PLift α)) := by
  intro x
  contrapose
  simpa [PLift.eq_up_iff_down_eq] using ha x.down

Result:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
this : mulSupport (f ∘ PLift.down) ⊆ ↑{{ down := a }}
⊢ ∏ᶠ (x : α), f x = f a

Proof state:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
x : PLift α
⊢ x ∈ mulSupport (f ∘ PLift.down) → x ∈ ↑{{ down := a }}

Tactic:
contrapose

Result:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
x : PLift α
⊢ x ∉ ↑{{ down := a }} → x ∉ mulSupport (f ∘ PLift.down)

Proof state:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
⊢ mulSupport (f ∘ PLift.down) ⊆ ↑{{ down := a }}

Tactic:
intro x

Result:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
x : PLift α
⊢ x ∈ mulSupport (f ∘ PLift.down) → x ∈ ↑{{ down := a }}

Proof state:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
this : mulSupport (f ∘ PLift.down) ⊆ ↑{{ down := a }}
⊢ ∏ᶠ (x : α), f x = f a

Tactic:
rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_singleton]

Result:
no goals

Proof state:
M : Type u_2
α : Sort u_4
inst✝ : CommMonoid M
f : α → M
a : α
ha : ∀ (x : α), x ≠ a → f x = 1
x : PLift α
⊢ x ∉ ↑{{ down := a }} → x ∉ mulSupport (f ∘ PLift.down)

Tactic:
simpa [PLift.eq_up_iff_down_eq] using ha x.down

Result:
no goals
-- Mathlib/Algebra/Ring/BooleanRing.lean
theorem sup_inf_self (a b : α) : a ⊔ a ⊓ b = a

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a + a * b + a * (a * b) = a

Tactic:
rw [← mul_assoc, mul_self, add_assoc, add_self, add_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Power2.lean
theorem nextPowerOfTwo_dec {n power : Nat} (h₁ : power > 0) (h₂ : power < n) : n - power * 2 < n - power

Proof state:
n power : Nat
h₁ : power > 0
h₂ : power < n
this : power * 2 = power + power
⊢ n - power - power < n - power

Tactic:
exact Nat.sub_lt (Nat.zero_lt_sub_of_lt h₂) h₁

Result:
no goals

Proof state:
n power : Nat
h₁ : power > 0
h₂ : power < n
⊢ power * 2 = power + power

Tactic:
simp_arith

Result:
no goals

Proof state:
n power : Nat
h₁ : power > 0
h₂ : power < n
⊢ n - power * 2 < n - power

Tactic:
have : power * 2 = power + power := by simp_arith

Result:
n power : Nat
h₁ : power > 0
h₂ : power < n
this : power * 2 = power + power
⊢ n - power * 2 < n - power

Proof state:
n power : Nat
h₁ : power > 0
h₂ : power < n
this : power * 2 = power + power
⊢ n - power * 2 < n - power

Tactic:
rw [this, Nat.sub_add_eq]

Result:
n power : Nat
h₁ : power > 0
h₂ : power < n
this : power * 2 = power + power
⊢ n - power - power < n - power
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean
lemma r1_pos : 0 < r1 z

Proof state:
z : ℍ
⊢ 0 < z.im ^ 2 / (z.re ^ 2 + z.im ^ 2)

Tactic:
positivity

Result:
no goals

Proof state:
z : ℍ
⊢ 0 < r1 z

Tactic:
dsimp only [r1]

Result:
z : ℍ
⊢ 0 < z.im ^ 2 / (z.re ^ 2 + z.im ^ 2)
-- Mathlib/Analysis/NormedSpace/Connected.lean
theorem isPathConnected_compl_of_one_lt_codim {E : Submodule ℝ F}
    (hcodim : 1 < Module.rank ℝ (F ⧸ E)) : IsPathConnected (Eᶜ : Set F)

Proof state:
case intro
F : Type u_1
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
E' : Submodule ℝ F
hE' : IsCompl E E'
⊢ IsPathConnected (↑E)ᶜ

Tactic:
refine isPathConnected_compl_of_isPathConnected_compl_zero hE'.symm
  (isPathConnected_compl_singleton_of_one_lt_rank ?_ 0)

Result:
case intro
F : Type u_1
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
E' : Submodule ℝ F
hE' : IsCompl E E'
⊢ 1 < Module.rank ℝ ↥E'

Proof state:
F : Type u_1
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
⊢ IsPathConnected (↑E)ᶜ

Tactic:
rcases E.exists_isCompl with ⟨E', hE'⟩

Result:
case intro
F : Type u_1
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
E' : Submodule ℝ F
hE' : IsCompl E E'
⊢ IsPathConnected (↑E)ᶜ

Proof state:
case intro
F : Type u_1
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
E' : Submodule ℝ F
hE' : IsCompl E E'
⊢ 1 < Module.rank ℝ ↥E'

Tactic:
rwa [← (E.quotientEquivOfIsCompl E' hE').rank_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem_set_self {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) :
    (l.set i a)[i] = a :=
  match l, i with
  | [], _ => by
    simp at h
  | _ :: _, 0 => by simp
  | _ :: l, i + 1 => by simp [getElem_set_self]

Proof state:
α : Type u_1
l : List α
i : Nat
a head✝ : α
tail✝ : List α
h : 0 < ((head✝ :: tail✝).set 0 a).length
⊢ ((head✝ :: tail✝).set 0 a)[0] = a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l✝ : List α
i✝ : Nat
a head✝ : α
l : List α
i : Nat
h : i + 1 < ((head✝ :: l).set (i + 1) a).length
⊢ ((head✝ :: l).set (i + 1) a)[i + 1] = a

Tactic:
simp [getElem_set_self]

Result:
no goals

Proof state:
α : Type u_1
l : List α
i : Nat
a : α
x✝ : Nat
h : x✝ < ([].set x✝ a).length
⊢ ([].set x✝ a)[x✝] = a

Tactic:
simp at h

Result:
no goals
-- Mathlib/Algebra/Lie/Solvable.lean
theorem abelian_iff_derived_one_eq_bot : IsLieAbelian I ↔ derivedSeriesOfIdeal R L 1 I = ⊥

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ IsLieAbelian ↥I ↔ D 1 I = ⊥

Tactic:
rw [derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_zero,
  LieSubmodule.lie_abelian_iff_lie_self_eq_bot]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/List.lean
@[to_additive sum_le_card_nsmul]
lemma prod_le_pow_card [Preorder M] [MulRightMono M]
    [MulLeftMono M] (l : List M) (n : M) (h : ∀ x ∈ l, x ≤ n) :
    l.prod ≤ n ^ l.length

Proof state:
M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l : List M
n : M
h : ∀ (x : M), x ∈ l → x ≤ n
⊢ l.prod ≤ n ^ l.length

Tactic:
simpa only [map_id', map_const', prod_replicate] using prod_le_prod' h

Result:
no goals
-- Mathlib/Algebra/CharP/CharAndCard.lean
theorem isUnit_iff_not_dvd_char_of_ringChar_ne_zero (R : Type*) [CommRing R] (p : ℕ) [Fact p.Prime]
    (hR : ringChar R ≠ 0) : IsUnit (p : R) ↔ ¬p ∣ ringChar R

Proof state:
case intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
r : ℕ
hq : ringChar R = ringChar R * (p * r)
hr : q = ringChar R * r
⊢ False

Tactic:
nth_rw 1 [← mul_one (ringChar R)] at hq

Result:
case intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
r : ℕ
hq : ringChar R * 1 = ringChar R * (p * r)
hr : q = ringChar R * r
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
⊢ IsUnit ↑p ↔ ¬p ∣ ringChar R

Tactic:
have hp : p.Prime := Fact.out

Result:
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
⊢ IsUnit ↑p ↔ ¬p ∣ ringChar R

Proof state:
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
h₄ : ¬↑(ringChar R) ∣ ↑q → ¬↑↑q = 0
hq : a * ↑(ringChar R) = a * ↑(p * q)
⊢ False

Tactic:
rw [Nat.cast_mul, hch, mul_zero, ← mul_assoc, ha, one_mul] at hq

Result:
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
h₄ : ¬↑(ringChar R) ∣ ↑q → ¬↑↑q = 0
hq : 0 = ↑q
⊢ False

Proof state:
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
h₄ : ¬↑(ringChar R) ∣ ↑q → ¬↑↑q = 0
hq : 0 = ↑q
⊢ False

Tactic:
norm_cast at h₄

Result:
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
hq : 0 = ↑q
h₄ : ¬ringChar R ∣ q → ¬↑q = 0
⊢ False

Proof state:
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
⊢ False

Tactic:
have h₃ : ¬ringChar R ∣ q := by
  rintro ⟨r, hr⟩
  rw [hr, ← mul_assoc, mul_comm p, mul_assoc] at hq
  nth_rw 1 [← mul_one (ringChar R)] at hq
  exact Nat.Prime.not_dvd_one hp ⟨r, mul_left_cancel₀ hR hq⟩

Result:
case mp.intro.intro
R : Type u_1
inst✝¹ : CommRing R
p : ℕ
inst✝ : Fact (Nat.Prime p)
hR : ringChar R ≠ 0
hch : ↑(ringChar R) = 0
hp : Nat.Prime p
h₁ : IsUnit ↑p
q : ℕ
hq : ringChar R = p * q
a : R
ha : a * ↑p = 1
h₃ : ¬ringChar R ∣ q
⊢ False
-- Mathlib/RingTheory/FractionalIdeal/Extended.lean
@[simp]
lemma coe_extended_eq_span : I.extended L hf = span B (map_f '' I)

Proof state:
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
⊢ ↑(extended L hf I) = span B (⇑(IsLocalization.map L f hf) '' ↑I)

Tactic:
ext

Result:
case h
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
x✝ : L
⊢ x✝ ∈ ↑(extended L hf I) ↔ x✝ ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)

Proof state:
case h
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
I : FractionalIdeal M K
x✝ : L
⊢ x✝ ∈ ↑(extended L hf I) ↔ x✝ ∈ span B (⇑(IsLocalization.map L f hf) '' ↑I)

Tactic:
simp [mem_coe, mem_extended_iff]

Result:
no goals
-- Mathlib/Algebra/Lie/Classical.lean
theorem soIndefiniteEquiv_apply {i : R} (hi : i * i = -1) (A : so' p q R) :
    (soIndefiniteEquiv p q R hi A : Matrix (p ⊕ q) (p ⊕ q) R) =
      (Pso p q R i)⁻¹ * (A : Matrix (p ⊕ q) (p ⊕ q) R) * Pso p q R i

Proof state:
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
A : ↥(so' p q R)
⊢ ↑((skewAdjointMatricesLieSubalgebraEquiv (indefiniteDiagonal p q R) (Pso p q R i) (invertiblePso p q R hi)) A) =
    (Pso p q R i)⁻¹ * ↑A * Pso p q R i

Tactic:
erw [skewAdjointMatricesLieSubalgebraEquiv_apply]

Result:
no goals

Proof state:
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
A : ↥(so' p q R)
⊢ ↑((soIndefiniteEquiv p q R hi) A) = (Pso p q R i)⁻¹ * ↑A * Pso p q R i

Tactic:
rw [soIndefiniteEquiv, LieEquiv.trans_apply, LieEquiv.ofEq_apply]

Result:
p : Type u_2
q : Type u_3
R : Type u₂
inst✝⁴ : DecidableEq p
inst✝³ : DecidableEq q
inst✝² : CommRing R
inst✝¹ : Fintype p
inst✝ : Fintype q
i : R
hi : i * i = -1
A : ↥(so' p q R)
⊢ ↑((skewAdjointMatricesLieSubalgebraEquiv (indefiniteDiagonal p q R) (Pso p q R i) (invertiblePso p q R hi)) A) =
    (Pso p q R i)⁻¹ * ↑A * Pso p q R i
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem inv_singleton (a : α) : ({a} : Set α)⁻¹ = {a⁻¹}

Proof state:
α : Type u_2
inst✝ : InvolutiveInv α
a : α
⊢ {a}⁻¹ = {a⁻¹}

Tactic:
rw [← image_inv_eq_inv, image_singleton]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem LinearMap.toLinearMap₂'Aux_toMatrix₂Aux (f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂) :
    Matrix.toLinearMap₂'Aux σ₁ σ₂
        (LinearMap.toMatrix₂Aux R (fun i => Pi.single i 1) (fun j => Pi.single j 1) f) =
      f

Proof state:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring S₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring S₂
inst✝¹⁰ : AddCommMonoid N₂
inst✝⁹ : Module R N₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂
⊢ toLinearMap₂'Aux σ₁ σ₂ ((toMatrix₂Aux R (fun i => Pi.single i 1) fun j => Pi.single j 1) f) = f

Tactic:
refine ext_basis (Pi.basisFun R₁ n) (Pi.basisFun R₂ m) fun i j => ?_

Result:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring S₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring S₂
inst✝¹⁰ : AddCommMonoid N₂
inst✝⁹ : Module R N₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂
i : n
j : m
⊢ ((toLinearMap₂'Aux σ₁ σ₂ ((toMatrix₂Aux R (fun i => Pi.single i 1) fun j => Pi.single j 1) f)) ((Pi.basisFun R₁ n) i))
      ((Pi.basisFun R₂ m) j) =
    (f ((Pi.basisFun R₁ n) i)) ((Pi.basisFun R₂ m) j)

Proof state:
R : Type u_1
R₁ : Type u_2
S₁ : Type u_3
R₂ : Type u_4
S₂ : Type u_5
N₂ : Type u_10
n : Type u_11
m : Type u_12
inst✝¹⁵ : CommSemiring R
inst✝¹⁴ : Semiring R₁
inst✝¹³ : Semiring S₁
inst✝¹² : Semiring R₂
inst✝¹¹ : Semiring S₂
inst✝¹⁰ : AddCommMonoid N₂
inst✝⁹ : Module R N₂
inst✝⁸ : Module S₁ N₂
inst✝⁷ : Module S₂ N₂
inst✝⁶ : SMulCommClass S₁ R N₂
inst✝⁵ : SMulCommClass S₂ R N₂
inst✝⁴ : SMulCommClass S₂ S₁ N₂
σ₁ : R₁ →+* S₁
σ₂ : R₂ →+* S₂
inst✝³ : Fintype n
inst✝² : Fintype m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
f : (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂
i : n
j : m
⊢ ((toLinearMap₂'Aux σ₁ σ₂ ((toMatrix₂Aux R (fun i => Pi.single i 1) fun j => Pi.single j 1) f)) ((Pi.basisFun R₁ n) i))
      ((Pi.basisFun R₂ m) j) =
    (f ((Pi.basisFun R₁ n) i)) ((Pi.basisFun R₂ m) j)

Tactic:
simp_rw [Pi.basisFun_apply, Matrix.toLinearMap₂'Aux_single, LinearMap.toMatrix₂Aux_apply]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem not_equiv_zero_const_of_nonzero {q : ℚ} (hq : q ≠ 0) : ¬const (padicNorm p) q ≈ 0 :=
  fun h : LimZero (const (padicNorm p) q - 0) ↦
    not_limZero_const_of_nonzero (p := p) hq <| by simpa using h

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ
hq : q ≠ 0
h : (const (padicNorm p) q - 0).LimZero
⊢ (const (padicNorm p) q).LimZero

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem le_opNNNorm (f : ContinuousMultilinearMap 𝕜 E G) (m : ∀ i, E i) :
    ‖f m‖₊ ≤ ‖f‖₊ * ∏ i, ‖m i‖₊ :=
  NNReal.coe_le_coe.1 <| by
    push_cast
    exact f.le_opNorm m

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ ↑‖f m‖₊ ≤ ↑(‖f‖₊ * ∏ i : ι, ‖m i‖₊)

Tactic:
push_cast

Result:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ ‖f m‖ ≤ ‖f‖ * ∏ x : ι, ‖m x‖

Proof state:
𝕜 : Type u
ι : Type v
E : ι → Type wE
G : Type wG
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : SeminormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
inst✝ : Fintype ι
f : ContinuousMultilinearMap 𝕜 E G
m : (i : ι) → E i
⊢ ‖f m‖ ≤ ‖f‖ * ∏ x : ι, ‖m x‖

Tactic:
exact f.le_opNorm m

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem HasFDerivAtFilter.sum (h : ∀ i ∈ u, HasFDerivAtFilter (A i) (A' i) x L) :
    HasFDerivAtFilter (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x L

Proof state:
case h.e'_7.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
L : Filter E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, (fun x' => A i x' - A i x - (A' i) (x' - x)) =o[L] fun x' => x' - x
x✝ : E
⊢ ∑ i ∈ u, A i x✝ - ∑ i ∈ u, A i x - (∑ i ∈ u, A' i) (x✝ - x) = ∑ i ∈ u, (A i x✝ - A i x - (A' i) (x✝ - x))

Tactic:
simp [ContinuousLinearMap.sum_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
L : Filter E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, (fun x' => A i x' - A i x - (A' i) (x' - x)) =o[L] fun x' => x' - x
⊢ (fun x' => ∑ i ∈ u, A i x' - ∑ i ∈ u, A i x - (∑ i ∈ u, A' i) (x' - x)) =o[L] fun x' => x' - x

Tactic:
convert IsLittleO.sum h

Result:
case h.e'_7.h
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
L : Filter E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, (fun x' => A i x' - A i x - (A' i) (x' - x)) =o[L] fun x' => x' - x
x✝ : E
⊢ ∑ i ∈ u, A i x✝ - ∑ i ∈ u, A i x - (∑ i ∈ u, A' i) (x✝ - x) = ∑ i ∈ u, (A i x✝ - A i x - (A' i) (x✝ - x))

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
L : Filter E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, HasFDerivAtFilter (A i) (A' i) x L
⊢ HasFDerivAtFilter (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) x L

Tactic:
simp only [hasFDerivAtFilter_iff_isLittleO] at *

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
L : Filter E
ι : Type u_4
u : Finset ι
A : ι → E → F
A' : ι → E →L[𝕜] F
h : ∀ i ∈ u, (fun x' => A i x' - A i x - (A' i) (x' - x)) =o[L] fun x' => x' - x
⊢ (fun x' => ∑ i ∈ u, A i x' - ∑ i ∈ u, A i x - (∑ i ∈ u, A' i) (x' - x)) =o[L] fun x' => x' - x
-- Mathlib/Order/UpperLower/Basic.lean
lemma IsLowerSet.erase (hs : IsLowerSet s) (has : ∀ b ∈ s, a ≤ b → b = a) : IsLowerSet (s \ {a}) :=
  hs.sdiff <| by simpa using has

Proof state:
α : Type u_1
inst✝ : LE α
s : Set α
a : α
hs : IsLowerSet s
has : ∀ b ∈ s, a ≤ b → b = a
⊢ ∀ b ∈ s, ∀ c ∈ {a}, c ≤ b → b ∈ {a}

Tactic:
simpa using has

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem ball_eq_singleton_of_subsingleton [Subsingleton α] (h : 0 < ε) : ball x ε = {x}

Proof state:
α : Type u
inst✝¹ : PseudoMetricSpace α
x : α
ε : ℝ
inst✝ : Subsingleton α
h : 0 < ε
⊢ ball x ε = {x}

Tactic:
ext x'

Result:
case h
α : Type u
inst✝¹ : PseudoMetricSpace α
x : α
ε : ℝ
inst✝ : Subsingleton α
h : 0 < ε
x' : α
⊢ x' ∈ ball x ε ↔ x' ∈ {x}

Proof state:
case h
α : Type u
inst✝¹ : PseudoMetricSpace α
x : α
ε : ℝ
inst✝ : Subsingleton α
h : 0 < ε
x' : α
⊢ x' ∈ ball x ε ↔ x' ∈ {x}

Tactic:
simpa [Subsingleton.allEq x x']

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem subperm_cons_diff {a : α} {l₁ l₂ : List α} : (a :: l₁).diff l₂ <+~ a :: l₁.diff l₂

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ : List α
⊢ (a :: l₁).diff [] <+~ a :: l₁.diff []

Tactic:
exact ⟨a :: l₁, by simp [List.diff]⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ l₂ : List α
⊢ (a :: l₁).diff l₂ <+~ a :: l₁.diff l₂

Tactic:
induction l₂ with
| nil => exact ⟨a :: l₁, by simp [List.diff]⟩
| cons b l₂ ih =>
  rw [diff_cons, diff_cons, ← diff_erase, ← diff_erase]
  exact Subperm.trans (.erase _ ih) (erase_cons_subperm_cons_erase ..)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ : List α
⊢ a :: l₁ ~ (a :: l₁).diff [] ∧ a :: l₁ <+ a :: l₁.diff []

Tactic:
simp [List.diff]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ : List α
b : α
l₂ : List α
ih : (a :: l₁).diff l₂ <+~ a :: l₁.diff l₂
⊢ (a :: l₁).diff (b :: l₂) <+~ a :: l₁.diff (b :: l₂)

Tactic:
rw [diff_cons, diff_cons, ← diff_erase, ← diff_erase]

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ : List α
b : α
l₂ : List α
ih : (a :: l₁).diff l₂ <+~ a :: l₁.diff l₂
⊢ ((a :: l₁).diff l₂).erase b <+~ a :: (l₁.diff l₂).erase b

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
l₁ : List α
b : α
l₂ : List α
ih : (a :: l₁).diff l₂ <+~ a :: l₁.diff l₂
⊢ ((a :: l₁).diff l₂).erase b <+~ a :: (l₁.diff l₂).erase b

Tactic:
exact Subperm.trans (.erase _ ih) (erase_cons_subperm_cons_erase ..)

Result:
no goals