harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/FintypeCat.lean
@[simp]
lemma productEquiv_symm_comp_π_apply {ι : Type*} [Finite ι] (X : ι → FintypeCat.{u})
    (x : ∀ i, X i) (i : ι) : Pi.π X i ((productEquiv X).symm x) = x i

Proof state:
ι : Type u_1
inst✝ : Finite ι
X : ι → FintypeCat
x : (i : ι) → (X i).carrier
i : ι
⊢ Pi.π X i ((productEquiv X).symm x) = x i

Tactic:
rw [← productEquiv_apply, Equiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.ne_zero {v : ι → E} (hv : Orthonormal 𝕜 v) (i : ι) : v i ≠ 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
i : ι
⊢ v i ≠ 0

Tactic:
refine ne_of_apply_ne norm ?_

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
i : ι
⊢ ‖v i‖ ≠ ‖0‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
i : ι
⊢ 1 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
i : ι
⊢ ‖v i‖ ≠ ‖0‖

Tactic:
rw [hv.1 i, norm_zero]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
i : ι
⊢ 1 ≠ 0
-- Mathlib/CategoryTheory/MorphismProperty/Comma.lean
@[simp]
lemma eqToHom_right {X Y : P.Comma L R Q W} (h : X = Y) :
    (eqToHom h).right = eqToHom (by rw [h])

Proof state:
A : Type u_1
inst✝⁴ : Category.{?u.85400, u_1} A
B : Type u_2
inst✝³ : Category.{?u.85407, u_2} B
T : Type u_3
inst✝² : Category.{?u.85414, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
⊢ X.right = Y.right

Tactic:
rw [h]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁴ : Category.{u_4, u_1} A
B : Type u_2
inst✝³ : Category.{u_5, u_2} B
T : Type u_3
inst✝² : Category.{u_6, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
X : MorphismProperty.Comma L R P Q W
⊢ (eqToHom ⋯).right = eqToHom ⋯

Tactic:
rfl

Result:
no goals

Proof state:
A : Type u_1
inst✝⁴ : Category.{u_4, u_1} A
B : Type u_2
inst✝³ : Category.{u_5, u_2} B
T : Type u_3
inst✝² : Category.{u_6, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
X Y : MorphismProperty.Comma L R P Q W
h : X = Y
⊢ (eqToHom h).right = eqToHom ⋯

Tactic:
subst h

Result:
A : Type u_1
inst✝⁴ : Category.{u_4, u_1} A
B : Type u_2
inst✝³ : Category.{u_5, u_2} B
T : Type u_3
inst✝² : Category.{u_6, u_3} T
L : A ⥤ T
R : B ⥤ T
P : MorphismProperty T
Q : MorphismProperty A
W : MorphismProperty B
inst✝¹ : Q.IsMultiplicative
inst✝ : W.IsMultiplicative
X : MorphismProperty.Comma L R P Q W
⊢ (eqToHom ⋯).right = eqToHom ⋯
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem dite_eq_left_iff {p : Prop} [Decidable p] {x : α} {y : ¬ p → α} : (if h : p then x else y h) = x ↔ ∀ h : ¬ p, y h = x

Proof state:
α : Sort u_1
p : Prop
inst✝ : Decidable p
x : α
y : ¬p → α
⊢ (if h : p then x else y h) = x ↔ ∀ (h : ¬p), y h = x

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem mul_one (χ : MulChar R R') : χ * 1 = χ

Proof state:
case h
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a✝ : Rˣ
⊢ (χ * 1) ↑a✝ = χ ↑a✝

Tactic:
simp only [mul_one, Pi.mul_apply, MulChar.coeToFun_mul, MulChar.one_apply_coe]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
⊢ χ * 1 = χ

Tactic:
ext

Result:
case h
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a✝ : Rˣ
⊢ (χ * 1) ↑a✝ = χ ↑a✝
-- Mathlib/Analysis/Convex/Segment.lean
theorem openSegment_same (x : E) : openSegment 𝕜 x x = {x} :=
  Set.ext fun z =>
    ⟨fun ⟨a, b, _, _, hab, hz⟩ => by
      simpa only [← add_smul, mem_singleton_iff, hab, one_smul, eq_comm] using hz,
    fun h : z = x => by
      obtain ⟨a, ha₀, ha₁⟩ := DenselyOrdered.dense (0 : 𝕜) 1 zero_lt_one
      refine ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel _ _, ?_⟩
      rw [← add_smul, add_sub_cancel, one_smul, h]⟩

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ z ∈ openSegment 𝕜 x x

Tactic:
refine ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel _ _, ?_⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ a • x + (1 - a) • x = z

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ a • x + (1 - a) • x = z

Tactic:
rw [← add_smul, add_sub_cancel, one_smul, h]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
h : z = x
⊢ z ∈ openSegment 𝕜 x x

Tactic:
obtain ⟨a, ha₀, ha₁⟩ := DenselyOrdered.dense (0 : 𝕜) 1 zero_lt_one

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
h : z = x
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ z ∈ openSegment 𝕜 x x

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nontrivial 𝕜
inst✝ : DenselyOrdered 𝕜
x z : E
x✝ : z ∈ openSegment 𝕜 x x
a b : 𝕜
left✝¹ : 0 < a
left✝ : 0 < b
hab : a + b = 1
hz : a • x + b • x = z
⊢ z ∈ {x}

Tactic:
simpa only [← add_smul, mem_singleton_iff, hab, one_smul, eq_comm] using hz

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem zero_mem_iff {a : A} : (0 : R) ∈ σ a ↔ ¬IsUnit a

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ 0 ∈ σ a ↔ ¬IsUnit a

Tactic:
rw [mem_iff, map_zero, zero_sub, IsUnit.neg_iff]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem isBigOWith_top : IsBigOWith c ⊤ f g ↔ ∀ x, ‖f x‖ ≤ c * ‖g x‖

Proof state:
α : Type u_1
E : Type u_3
F : Type u_4
inst✝¹ : Norm E
inst✝ : Norm F
c : ℝ
f : α → E
g : α → F
⊢ IsBigOWith c ⊤ f g ↔ ∀ (x : α), ‖f x‖ ≤ c * ‖g x‖

Tactic:
rw [IsBigOWith_def, eventually_top]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem translate_iterate (x : ℝ) (n : ℕ) :
    (translate (Multiplicative.ofAdd x))^[n] = translate (Multiplicative.ofAdd <| ↑n * x)

Proof state:
x : ℝ
n : ℕ
⊢ (⇑↑(translate (Multiplicative.ofAdd x)))^[n] = ⇑↑(translate (Multiplicative.ofAdd (↑n * x)))

Tactic:
rw [← coe_pow, ← Units.val_pow_eq_pow_val, translate_pow]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem toList_filterRevM [Monad m] [LawfulMonad m] (a : Array α) (p : α → m Bool) :
    toList <$> a.filterRevM p = a.toList.filterRevM p

Proof state:
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
p : α → m Bool
⊢ toList <$> filterRevM p a = List.filterRevM p a.toList

Tactic:
rw [List.filterRevM_toArray]

Result:
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
p : α → m Bool
⊢ toList <$> List.toArray <$> List.filterRevM p a.toList = List.filterRevM p a.toList

Proof state:
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
p : α → m Bool
⊢ toList <$> List.toArray <$> List.filterRevM p a.toList = List.filterRevM p a.toList

Tactic:
simp only [Functor.map_map, id_map']

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma b₄_of_char_two : W.b₄ = W.a₁ * W.a₃

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ W.b₄ = W.a₁ * W.a₃

Tactic:
rw [b₄]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ 2 * W.a₄ + W.a₁ * W.a₃ = W.a₁ * W.a₃

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 2
⊢ 2 * W.a₄ + W.a₁ * W.a₃ = W.a₁ * W.a₃

Tactic:
linear_combination W.a₄ * CharP.cast_eq_zero R 2

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem coe_mul_inv_eq_one {n : ℕ} (x : ℕ) (h : Nat.Coprime x n) :
    ((x : ZMod n) * (x : ZMod n)⁻¹) = 1

Proof state:
n x : ℕ
h : (x % n).gcd n = 1
⊢ ↑x * (↑x)⁻¹ = 1

Tactic:
rw [mul_inv_eq_gcd, val_natCast, h, Nat.cast_one]

Result:
no goals

Proof state:
n x : ℕ
h : x.Coprime n
⊢ ↑x * (↑x)⁻¹ = 1

Tactic:
rw [Nat.Coprime, Nat.gcd_comm, Nat.gcd_rec] at h

Result:
n x : ℕ
h : (x % n).gcd n = 1
⊢ ↑x * (↑x)⁻¹ = 1
-- Mathlib/Algebra/CharP/Two.lean
theorem sum_mul_self (s : Finset ι) (f : ι → R) :
    ((∑ i ∈ s, f i) * ∑ i ∈ s, f i) = ∑ i ∈ s, f i * f i

Proof state:
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CharP R 2
s : Finset ι
f : ι → R
⊢ (∑ i ∈ s, f i) * ∑ i ∈ s, f i = ∑ i ∈ s, f i * f i

Tactic:
simp_rw [← pow_two, sum_sq]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem Equiv.Perm.decomposeFin_symm_apply_zero {n : ℕ} (p : Fin (n + 1)) (e : Perm (Fin n)) :
    Equiv.Perm.decomposeFin.symm (p, e) 0 = p

Proof state:
n : ℕ
p : Fin (n + 1)
e : Perm (Fin n)
⊢ (decomposeFin.symm (p, e)) 0 = p

Tactic:
simp [Equiv.Perm.decomposeFin]

Result:
no goals
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem pow_card {p : ℕ} [Fact p.Prime] (x : ZMod p) : x ^ p = x

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
h : x ^ Fintype.card (ZMod p) = x
⊢ x ^ p = x

Tactic:
rwa [ZMod.card p] at h

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
⊢ x ^ p = x

Tactic:
have h := FiniteField.pow_card x

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
h : x ^ Fintype.card (ZMod p) = x
⊢ x ^ p = x
-- Mathlib/Topology/Separation/Basic.lean
theorem R1Space.inf {X : Type*} {t₁ t₂ : TopologicalSpace X}
    (h₁ : @R1Space X t₁) (h₂ : @R1Space X t₂) : @R1Space X (t₁ ⊓ t₂)

Proof state:
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : R1Space X
h₂ : R1Space X
⊢ R1Space X

Tactic:
apply R1Space.iInf

Result:
case ht
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : R1Space X
h₂ : R1Space X
⊢ ∀ (i : Bool), R1Space X

Proof state:
case ht
X : Type u_3
t₁ t₂ : TopologicalSpace X
h₁ : R1Space X
h₂ : R1Space X
⊢ ∀ (i : Bool), R1Space X

Tactic:
simp [*]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
private lemma toAffine_add_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Nonsingular P)
    (hQ : W.Nonsingular Q) (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
    (hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)) : toAffine W
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1] = toAffine W P + toAffine W Q

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
⊢ ¬(P x / P z ^ 2 = Q x / Q z ^ 2 ∧ P y / P z ^ 3 = (Jacobian.toAffine W).negY (Q x / Q z ^ 2) (Q y / Q z ^ 3))

Tactic:
rwa [← X_eq_iff hPz hQz, ← Y_eq_iff' hPz hQz]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z ^ 2 = Q x * P z ^ 2 ∧ P y * Q z ^ 3 = W.negY Q * P z ^ 3)
⊢ toAffine W
      ![(Jacobian.toAffine W).addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          ((Jacobian.toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        (Jacobian.toAffine W).addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          ((Jacobian.toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1] =
    toAffine W P + toAffine W Q

Tactic:
rw [toAffine_some <| nonsingular_add_of_Z_ne_zero hP hQ hPz hQz hxy, toAffine_of_Z_ne_zero hP hPz,
  toAffine_of_Z_ne_zero hQ hQz,
  Affine.Point.add_some <| by rwa [← X_eq_iff hPz hQz, ← Y_eq_iff' hPz hQz]]

Result:
no goals
-- Mathlib/Tactic/NormNum/BigOperators.lean
lemma Finset.range_succ' {n nn n' : ℕ} (pn : NormNum.IsNat n nn) (pn' : nn = Nat.succ n') :
    Finset.range n = Finset.cons n' (Finset.range n') Finset.not_mem_range_self

Proof state:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Finset.range n = Finset.cons n' (Finset.range n') ⋯

Tactic:
rw [pn.out, Nat.cast_id, pn', Finset.range_succ, Finset.insert_eq_cons]

Result:
no goals
-- Mathlib/Data/Multiset/Fintype.lean
lemma coe_consEquiv_of_eq_of_eq {v : α} (x : v ::ₘ m) (hx : ↑x = v) (hx2 : x.2 = m.count v) :
    consEquiv x = none

Proof state:
α : Type u_1
inst✝ : DecidableEq α
m : Multiset α
v : α
x : (v ::ₘ m).ToType
hx : x.fst = v
hx2 : ↑x.snd = count v m
⊢ consEquiv x = none

Tactic:
simp [consEquiv, hx, hx2]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Integral.lean
theorem integral_mul_right_eq_self [IsMulRightInvariant μ] (f : G → E) (g : G) :
    (∫ x, f (x * g) ∂μ) = ∫ x, f x ∂μ

Proof state:
G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
f : G → E
g : G
h_mul : MeasurableEmbedding fun x => x * g
⊢ ∫ (x : G), f (x * g) ∂μ = ∫ (x : G), f x ∂μ

Tactic:
rw [← h_mul.integral_map, map_mul_right_eq_self]

Result:
no goals

Proof state:
G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
f : G → E
g : G
⊢ ∫ (x : G), f (x * g) ∂μ = ∫ (x : G), f x ∂μ

Tactic:
have h_mul : MeasurableEmbedding fun x => x * g :=
  (MeasurableEquiv.mulRight g).measurableEmbedding

Result:
G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulRightInvariant
f : G → E
g : G
h_mul : MeasurableEmbedding fun x => x * g
⊢ ∫ (x : G), f (x * g) ∂μ = ∫ (x : G), f x ∂μ
-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
@[simp]
lemma residueClass_apply_zero : residueClass a 0 = 0

Proof state:
q : ℕ
a : ZMod q
⊢ residueClass a 0 = 0

Tactic:
simp only [Set.indicator_apply_eq_zero, Set.mem_setOf_eq, Nat.cast_zero, map_zero, ofReal_zero,
  implies_true]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem _root_.List.reverse_toArray (l : List α) : l.toArray.reverse = l.reverse.toArray

Proof state:
case h
α : Type u_1
l : List α
⊢ l.toArray.reverse.toList = l.reverse.toArray.toList

Tactic:
simp only [toList_reverse]

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ l.toArray.reverse = l.reverse.toArray

Tactic:
apply ext'

Result:
case h
α : Type u_1
l : List α
⊢ l.toArray.reverse.toList = l.reverse.toArray.toList
-- Mathlib/Algebra/Star/Module.lean
theorem IsSelfAdjoint.coe_selfAdjointPart_apply {x : A} (hx : IsSelfAdjoint x) :
    (selfAdjointPart R x : A) = x

Proof state:
R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
x : A
hx : IsSelfAdjoint x
⊢ ↑((selfAdjointPart R) x) = x

Tactic:
rw [selfAdjointPart_apply_coe, hx.star_eq, smul_add, invOf_two_smul_add_invOf_two_smul]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma IsGreatest.nnnorm_cfcₙ (f : 𝕜 → 𝕜) (a : A)
    (hf : ContinuousOn f (σₙ 𝕜 a)

Proof state:
case h.e'_4
𝕜 : 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
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σₙ 𝕜 a)) _auto✝
hf₀ : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ ‖cfcₙ f a‖₊ = ‖cfcₙ f a‖.toNNReal

Tactic:
simp [Set.image_image, norm_toNNReal]

Result:
no goals

Proof state:
case h.e'_3
𝕜 : 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
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σₙ 𝕜 a)) _auto✝
hf₀ : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ (fun x => ‖f x‖₊) '' σₙ 𝕜 a = Real.toNNReal '' ((fun x => ‖f x‖) '' σₙ 𝕜 a)

case h.e'_4
𝕜 : 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
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σₙ 𝕜 a)) _auto✝
hf₀ : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ ‖cfcₙ f a‖₊ = ‖cfcₙ f a‖.toNNReal

Tactic:
all_goals simp [Set.image_image, norm_toNNReal]

Result:
no goals

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
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σₙ 𝕜 a)) _auto✝
hf₀ : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ IsGreatest ((fun x => ‖f x‖₊) '' σₙ 𝕜 a) ‖cfcₙ f a‖₊

Tactic:
convert Real.toNNReal_mono.map_isGreatest (.norm_cfcₙ f a)

Result:
case h.e'_3
𝕜 : 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
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σₙ 𝕜 a)) _auto✝
hf₀ : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ (fun x => ‖f x‖₊) '' σₙ 𝕜 a = Real.toNNReal '' ((fun x => ‖f x‖) '' σₙ 𝕜 a)

case h.e'_4
𝕜 : 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
f : 𝕜 → 𝕜
a : A
hf : autoParam (ContinuousOn f (σₙ 𝕜 a)) _auto✝
hf₀ : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ ‖cfcₙ f a‖₊ = ‖cfcₙ f a‖.toNNReal
-- Mathlib/CategoryTheory/Monoidal/CoherenceLemmas.lean
theorem leftUnitor_tensor'' (X Y : C) :
    (α_ (𝟙_ C) X Y).hom ≫ (λ_ (X ⊗ Y)).hom = (λ_ X).hom ⊗ 𝟙 Y

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (α_ (𝟙_ C) X Y).hom ≫ (λ_ (X ⊗ Y)).hom = (λ_ X).hom ⊗ 𝟙 Y

Tactic:
monoidal_coherence

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RelabelNat.lean
theorem relabelNat_unsat_iff {entry : Entrypoint α} [Nonempty α] :
    (entry.relabelNat).Unsat ↔ entry.Unsat

Proof state:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
entry : Entrypoint α
inst✝ : Nonempty α
⊢ entry.relabelNat.Unsat ↔ entry.Unsat

Tactic:
simp only [Unsat, relabelNat]

Result:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
entry : Entrypoint α
inst✝ : Nonempty α
⊢ entry.aig.relabelNat.UnsatAt entry.ref.gate ⋯ ↔ entry.aig.UnsatAt entry.ref.gate ⋯

Proof state:
α : Type
inst✝² : DecidableEq α
inst✝¹ : Hashable α
entry : Entrypoint α
inst✝ : Nonempty α
⊢ entry.aig.relabelNat.UnsatAt entry.ref.gate ⋯ ↔ entry.aig.UnsatAt entry.ref.gate ⋯

Tactic:
rw [AIG.relabelNat_unsat_iff]

Result:
no goals
-- Mathlib/Data/Matrix/DoublyStochastic.lean
lemma mem_doublyStochastic_iff_sum :
    M ∈ doublyStochastic R n ↔
      (∀ i j, 0 ≤ M i j) ∧ (∀ i, ∑ j, M i j = 1) ∧ ∀ j, ∑ i, M i j = 1

Proof state:
R : Type u_1
n : Type u_2
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : OrderedSemiring R
M : Matrix n n R
⊢ M ∈ doublyStochastic R n ↔ (∀ (i j : n), 0 ≤ M i j) ∧ (∀ (i : n), ∑ j : n, M i j = 1) ∧ ∀ (j : n), ∑ i : n, M i j = 1

Tactic:
simp [funext_iff, doublyStochastic, mulVec, vecMul, dotProduct]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tdiv_add_tmod (a b : Int) : b * a.tdiv b + tmod a b = a

Proof state:
a b : Int
⊢ b * a.tdiv b + a.tmod b = a

Tactic:
rw [Int.add_comm]

Result:
a b : Int
⊢ a.tmod b + b * a.tdiv b = a

Proof state:
a b : Int
⊢ a.tmod b + b * a.tdiv b = a

Tactic:
apply tmod_add_tdiv ..

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
theorem alternatingProd_append :
    ∀ l₁ l₂ : List α,
      alternatingProd (l₁ ++ l₂) = alternatingProd l₁ * alternatingProd l₂ ^ (-1 : ℤ) ^ length l₁
  | [], l₂ => by simp
  | a :: l₁, l₂ => by
    simp_rw [cons_append, alternatingProd_cons, alternatingProd_append, length_cons, pow_succ',
      Int.neg_mul, one_mul, zpow_neg, ← div_eq_mul_inv, div_div]

Proof state:
α : Type u_2
inst✝ : CommGroup α
l₂ : List α
⊢ ([] ++ l₂).alternatingProd = [].alternatingProd * l₂.alternatingProd ^ (-1) ^ [].length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CommGroup α
a : α
l₁ l₂ : List α
⊢ (a :: l₁ ++ l₂).alternatingProd = (a :: l₁).alternatingProd * l₂.alternatingProd ^ (-1) ^ (a :: l₁).length

Tactic:
simp_rw [cons_append, alternatingProd_cons, alternatingProd_append, length_cons, pow_succ',
  Int.neg_mul, one_mul, zpow_neg, ← div_eq_mul_inv, div_div]

Result:
no goals