harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Basic.lean
/-- To show a property of all powers of `g` it suffices to show it is closed under multiplication
by `g` and `g⁻¹` on the right. For subgroups generated by more than one element, see
`Subgroup.closure_induction_right`. -/
@[to_additive "To show a property of all multiples of `g` it suffices to show it is closed under
addition by `g` and `-g` on the right. For additive subgroups generated by more than one element,
see `AddSubgroup.closure_induction_right`."]
lemma zpow_induction_right {g : G} {P : G → Prop} (h_one : P (1 : G))
    (h_mul : ∀ a, P a → P (a * g)) (h_inv : ∀ a, P a → P (a * g⁻¹)) (n : ℤ) : P (g ^ n)

Proof state:
case hn
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g ^ (-↑n - 1))

Tactic:
rw [zpow_sub_one]

Result:
case hn
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g ^ (-↑n) * g⁻¹)

Proof state:
case hz
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
⊢ P (g ^ 0)

Tactic:
rwa [zpow_zero]

Result:
no goals

Proof state:
case hp
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (g ^ ↑n)
⊢ P (g ^ (↑n + 1))

Tactic:
rw [zpow_add_one]

Result:
case hp
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (g ^ ↑n)
⊢ P (g ^ ↑n * g)

Proof state:
case hp
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (g ^ ↑n)
⊢ P (g ^ ↑n * g)

Tactic:
exact h_mul _ ih

Result:
no goals

Proof state:
case hn
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℕ
ih : P (g ^ (-↑n))
⊢ P (g ^ (-↑n) * g⁻¹)

Tactic:
exact h_inv _ ih

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
g : G
P : G → Prop
h_one : P 1
h_mul : ∀ (a : G), P a → P (a * g)
h_inv : ∀ (a : G), P a → P (a * g⁻¹)
n : ℤ
⊢ P (g ^ n)

Tactic:
induction n with
| hz => rwa [zpow_zero]
| hp n ih =>
  rw [zpow_add_one]
  exact h_mul _ ih
| hn n ih =>
  rw [zpow_sub_one]
  exact h_inv _ ih

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem mem_nhds_uniformity_iff_right {x : α} {s : Set α} :
    s ∈ 𝓝 x ↔ { p : α × α | p.1 = x → p.2 ∈ s } ∈ 𝓤 α

Proof state:
α : Type ua
inst✝ : UniformSpace α
x : α
s : Set α
⊢ s ∈ 𝓝 x ↔ {p | p.1 = x → p.2 ∈ s} ∈ 𝓤 α

Tactic:
simp only [nhds_eq_comap_uniformity, mem_comap_prod_mk]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Mod.lean
theorem mod_mul_left_div_self (m n k : Nat) : m % (k * n) / n = m / n % k

Proof state:
m n k : Nat
⊢ m % (k * n) / n = m / n % k

Tactic:
rw [Nat.mul_comm k n, mod_mul_right_div_self]

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts/FunctorCategory.lean
@[simp]
lemma leftUnitor_inv_app (F : J ⥤ C) (j : J) :
    (λ_ F).inv.app j = (λ_ (F.obj j)).inv

Proof state:
J : Type u_1
C : Type u_2
inst✝² : Category.{u_3, u_1} J
inst✝¹ : Category.{u_4, u_2} C
inst✝ : ChosenFiniteProducts C
F : J ⥤ C
j : J
⊢ (λ_ F).inv.app j = (λ_ (F.obj j)).inv

Tactic:
rw [← cancel_mono ((λ_ (F.obj j)).hom), Iso.inv_hom_id, ← leftUnitor_hom_app,
  Iso.inv_hom_id_app]

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem postcomp_map_heq (H : D ⥤ E) (hx : F.obj X = G.obj X) (hy : F.obj Y = G.obj Y)
    (hmap : HEq (F.map f) (G.map f)) : HEq ((F ⋙ H).map f) ((G ⋙ H).map f)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X Y : C
f : X ⟶ Y
H : D ⥤ E
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hmap : HEq (F.map f) (G.map f)
⊢ HEq ((F ⋙ H).map f) ((G ⋙ H).map f)

Tactic:
dsimp

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X Y : C
f : X ⟶ Y
H : D ⥤ E
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hmap : HEq (F.map f) (G.map f)
⊢ HEq (H.map (F.map f)) (H.map (G.map f))

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D
X Y : C
f : X ⟶ Y
H : D ⥤ E
hx : F.obj X = G.obj X
hy : F.obj Y = G.obj Y
hmap : HEq (F.map f) (G.map f)
⊢ HEq (H.map (F.map f)) (H.map (G.map f))

Tactic:
congr

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
lemma eval₂_minpolyDiv_self {T} [CommRing T] [Algebra R T] [IsDomain T] [DecidableEq T] (x : S)
    (σ₁ σ₂ : S →ₐ[R] T) :
    eval₂ σ₁ (σ₂ x) (minpolyDiv R x) =
      if σ₁ x = σ₂ x then σ₁ (aeval x (derivative <| minpoly R x)) else 0

Proof state:
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
σ₁ σ₂ : S →ₐ[R] T
⊢ eval₂ (↑σ₁) (σ₂ x) (minpolyDiv R x) = if σ₁ x = σ₂ x then σ₁ ((aeval x) (derivative (minpoly R x))) else 0

Tactic:
apply eval₂_minpolyDiv_of_eval₂_eq_zero

Result:
case hy
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
σ₁ σ₂ : S →ₐ[R] T
⊢ eval₂ ((↑σ₁).comp (algebraMap R S)) (σ₂ x) (minpoly R x) = 0

Proof state:
case hy
R : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : IsDomain T
inst✝ : DecidableEq T
x : S
σ₁ σ₂ : S →ₐ[R] T
⊢ eval₂ ((↑σ₁).comp (algebraMap R S)) (σ₂ x) (minpoly R x) = 0

Tactic:
rw [AlgHom.comp_algebraMap, ← σ₂.comp_algebraMap, ← eval₂_map, ← RingHom.coe_coe, eval₂_hom,
  eval_map, ← aeval_def, minpoly.aeval, map_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem SigmaFinite.of_map (μ : Measure α) {f : α → β} (hf : AEMeasurable f μ)
    (h : SigmaFinite (μ.map f)) : SigmaFinite μ :=
  ⟨⟨⟨fun n => f ⁻¹' spanningSets (μ.map f) n, fun _ => trivial, fun n => by
        simp only [← map_apply_of_aemeasurable hf, measurableSet_spanningSets,
          measure_spanningSets_lt_top],
        by rw [← preimage_iUnion, iUnion_spanningSets, preimage_univ]⟩⟩⟩

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
h : SigmaFinite (Measure.map f μ)
n : ℕ
⊢ μ ((fun n => f ⁻¹' spanningSets (Measure.map f μ) n) n) < ⊤

Tactic:
simp only [← map_apply_of_aemeasurable hf, measurableSet_spanningSets,
  measure_spanningSets_lt_top]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
h : SigmaFinite (Measure.map f μ)
⊢ ⋃ i, (fun n => f ⁻¹' spanningSets (Measure.map f μ) n) i = univ

Tactic:
rw [← preimage_iUnion, iUnion_spanningSets, preimage_univ]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Filter.lean
theorem henstock_le_mcShane : Henstock ≤ McShane

Proof state:
⊢ Henstock ≤ McShane

Tactic:
trivial

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
theorem map_star (a : A) : σ (star a) = star (σ a)

Proof state:
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
a : A
⊢ σ (star a) = star (σ a)

Tactic:
ext

Result:
case h
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
a : A
x✝ : R
⊢ x✝ ∈ σ (star a) ↔ x✝ ∈ star (σ a)

Proof state:
case h
R : Type u
A : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
inst✝² : InvolutiveStar R
inst✝¹ : StarRing A
inst✝ : StarModule R A
a : A
x✝ : R
⊢ x✝ ∈ σ (star a) ↔ x✝ ∈ star (σ a)

Tactic:
simpa only [Set.mem_star, mem_iff, not_iff_not] using star_mem_resolventSet_iff.symm

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/DotProduct.lean
lemma mul_conjTranspose_mul_self_eq_zero {p} (A : Matrix m n R) (B : Matrix p n R) :
    B * (Aᴴ * A) = 0 ↔ B * Aᴴ = 0

Proof state:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝⁶ : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : PartialOrder R
inst✝³ : NonUnitalRing R
inst✝² : StarRing R
inst✝¹ : StarOrderedRing R
inst✝ : NoZeroDivisors R
p : Type u_5
A : Matrix m n R
B : Matrix p n R
⊢ B * (Aᴴ * A) = 0 ↔ B * Aᴴ = 0

Tactic:
simpa only [conjTranspose_conjTranspose] using mul_self_mul_conjTranspose_eq_zero Aᴴ _

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
/-- Colex is an extension of the base order. -/
lemma singleton_lt_singleton : (toColex {a} : Colex α) < toColex {b} ↔ a < b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ { ofColex := {a} } < { ofColex := {b} } ↔ a < b

Tactic:
simp [toColex_lt_singleton]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem one_toType_eq (x : toType 1) : x = enum (· < ·) ⟨0, by simp⟩ :=
  Unique.eq_default x

Proof state:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
x : toType 1
⊢ 0 ∈ Iio (type fun x1 x2 => x1 < x2)

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Additive/ETransform.lean
theorem mulETransformLeft_inv : mulETransformLeft e⁻¹ x = (mulETransformRight e x.swap).swap

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ mulETransformLeft e⁻¹ x = (mulETransformRight e x.swap).swap

Tactic:
simp [-op_inv, op_smul_eq_smul, mulETransformLeft, mulETransformRight]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem rightAdjointMate_id {X : C} [HasRightDual X] : (𝟙 X)ᘁ = 𝟙 (Xᘁ)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X : C
inst✝ : HasRightDual X
⊢ 𝟙 Xᘁ = 𝟙 Xᘁ

Tactic:
simp [rightAdjointMate]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_alter [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.1)
    {a : α} {f : Option (β a) → Option (β a)} :
    Perm (toListModel (m.alter a f).1.2) (alterKey a f (toListModel m.1.2))

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
⊢ toListModel (m.alterₘ a f).val.buckets ~ alterKey a f (toListModel m.val.buckets)

Tactic:
exact toListModel_alterₘ h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
⊢ toListModel (m.alter a f).val.buckets ~ alterKey a f (toListModel m.val.buckets)

Tactic:
rw [alter_eq_alterₘ]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
⊢ toListModel (m.alterₘ a f).val.buckets ~ alterKey a f (toListModel m.val.buckets)
-- Mathlib/Algebra/Polynomial/Bivariate.lean
lemma map_mapRingHom_eval_map : (p.map <| mapRingHom f).eval (q.map f) = (p.eval q).map f

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X][Y]
q : R[X]
⊢ eval (map f q) (map (mapRingHom f) p) = map f (eval q p)

Tactic:
rw [eval_map, ← coe_mapRingHom, eval₂_hom]

Result:
no goals
-- Mathlib/Computability/TMToPartrec.lean
theorem codeSupp_case (f g k) :
    codeSupp (Code.case f g) k =
      trStmts₁ (trNormal (Code.case f g) k) ∪ (codeSupp f k ∪ codeSupp g k)

Proof state:
f g : Code
k : Cont'
⊢ codeSupp (f.case g) k = trStmts₁ (trNormal (f.case g) k) ∪ (codeSupp f k ∪ codeSupp g k)

Tactic:
simp [codeSupp, codeSupp', contSupp, Finset.union_assoc, Finset.union_left_comm]

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
theorem stdBasisMatrix_eq_of_single_single (i : m) (j : n) (a : α) :
    stdBasisMatrix i j a = Matrix.of (Pi.single i (Pi.single j a))

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
a : α
⊢ stdBasisMatrix i j a = of (Pi.single i (Pi.single j a))

Tactic:
ext a b

Result:
case a
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
a✝ : α
a : m
b : n
⊢ stdBasisMatrix i j a✝ a b = of (Pi.single i (Pi.single j a✝)) a b

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
a✝ : α
a : m
b : n
⊢ of (fun i' j' => if i = i' ∧ j = j' then a✝ else 0) a b = of (Pi.single i (Pi.single j a✝)) a b

Tactic:
by_cases hi : i = a <;> by_cases hj : j = b <;> simp [*]

Result:
no goals

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
a✝ : α
a : m
b : n
⊢ stdBasisMatrix i j a✝ a b = of (Pi.single i (Pi.single j a✝)) a b

Tactic:
unfold stdBasisMatrix

Result:
case a
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
a✝ : α
a : m
b : n
⊢ of (fun i' j' => if i = i' ∧ j = j' then a✝ else 0) a b = of (Pi.single i (Pi.single j a✝)) a b
-- Mathlib/Data/Set/Prod.lean
theorem prod_inter : s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂

Proof state:
case h.mk
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t₁ ∩ t₂) ↔ (x, y) ∈ s ×ˢ t₁ ∩ s ×ˢ t₂

Tactic:
simp only [← and_and_left, mem_inter_iff, mem_prod]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
⊢ s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
s : Set α
t₁ t₂ : Set β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t₁ ∩ t₂) ↔ (x, y) ∈ s ×ˢ t₁ ∩ s ×ˢ t₂
-- Mathlib/Algebra/Group/Basic.lean
theorem one_div_mul_one_div_rev : 1 / a * (1 / b) = 1 / (b * a)

Proof state:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
⊢ 1 / a * (1 / b) = 1 / (b * a)

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem coord_self : (coord R M x h) (⟨x, Submodule.mem_span_singleton_self x⟩ : R ∙ x) = 1

Proof state:
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
x : M
h : x ≠ 0
⊢ (coord R M x h) ⟨x, ⋯⟩ = 1

Tactic:
rw [← toSpanNonzeroSingleton_one R M x h, LinearEquiv.symm_apply_apply]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
@[simp] lemma erase_eq : s.erase a = s ↔ a ∉ s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : LowerSet α
a : α
⊢ s.erase a = s ↔ a ∉ s

Tactic:
rw [← sdiff_singleton]

Result:
α : Type u_1
inst✝ : Preorder α
s : LowerSet α
a : α
⊢ s.sdiff {a} = s ↔ a ∉ s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : LowerSet α
a : α
⊢ s.sdiff {a} = s ↔ a ∉ s

Tactic:
simp [-sdiff_singleton]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem multiplicity_eq_factorization {n p : ℕ} (pp : p.Prime) (hn : n ≠ 0) :
    multiplicity p n = n.factorization p

Proof state:
n p : ℕ
pp : Prime p
hn : n ≠ 0
⊢ multiplicity p n = n.factorization p

Tactic:
simp [factorization, pp, padicValNat_def' pp.ne_one hn.bot_lt]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} (h : m.WF) :
    k' ∈ Const.alter m k f ↔ if k == k' then (f (Const.get? m k)).isSome = true else k' ∈ m

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : Option β → Option β
h : m.WF
⊢ k' ∈ alter m k f ↔ if (k == k') = true then (f (get? m k)).isSome = true else k' ∈ m

Tactic:
simp only [mem_iff_contains, contains_alter h, Bool.ite_eq_true_distrib]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/AssocList.lean
theorem length_mapVal : (mapVal f l).length = l.length

Proof state:
α✝ : Type u_1
β✝¹ : Type u_2
β✝ : Type u_3
f : α✝ → β✝¹ → β✝
l : AssocList α✝ β✝¹
⊢ (mapVal f l).length = l.length

Tactic:
induction l <;> simp_all

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem _root_.List.aestronglyMeasurable_prod
    (l : List (α → M)) (hl : ∀ f ∈ l, AEStronglyMeasurable f μ) :
    AEStronglyMeasurable (fun x => (l.map fun f : α → M => f x).prod) μ

Proof state:
α : Type u_1
m₀ : MeasurableSpace α
μ : Measure α
M : Type u_5
inst✝² : Monoid M
inst✝¹ : TopologicalSpace M
inst✝ : ContinuousMul M
l : List (α → M)
hl : ∀ f ∈ l, AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x => (List.map (fun f => f x) l).prod) μ

Tactic:
simpa only [← Pi.list_prod_apply] using l.aestronglyMeasurable_prod' hl

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZetaValues.lean
theorem riemannZeta_neg_nat_eq_bernoulli (k : ℕ) :
    riemannZeta (-k) = (-1 : ℂ) ^ k * bernoulli (k + 1) / (k + 1)

Proof state:
k : ℕ
⊢ riemannZeta (-↑k) = (-1) ^ k * ↑(bernoulli (k + 1)) / (↑k + 1)

Tactic:
rw [riemannZeta_neg_nat_eq_bernoulli', bernoulli, Rat.cast_mul, Rat.cast_pow, Rat.cast_neg,
  Rat.cast_one, ← neg_one_mul, ← mul_assoc, pow_succ, ← mul_assoc, ← mul_pow, neg_one_mul (-1),
  neg_neg, one_pow, one_mul]

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
@[simp] lemma num_divNat_den (q : ℚ≥0) : divNat q.num q.den = q :=
  ext <| by rw [← (q : ℚ).mkRat_num_den']; simp [num_coe, den_coe]

Proof state:
q : ℚ≥0
⊢ ↑(divNat q.num q.den) = ↑q

Tactic:
rw [← (q : ℚ).mkRat_num_den']

Result:
q : ℚ≥0
⊢ ↑(divNat q.num q.den) = mkRat (↑q).num (↑q).den

Proof state:
q : ℚ≥0
⊢ ↑(divNat q.num q.den) = mkRat (↑q).num (↑q).den

Tactic:
simp [num_coe, den_coe]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem div_eq_div_iff_div_eq_div : a / b = c / d ↔ a / c = b / d

Proof state:
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ a / b = c / d ↔ a / c = b / d

Tactic:
rw [div_eq_iff_eq_mul, div_mul_eq_mul_div, div_eq_iff_eq_mul', mul_div_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem append_ne_nil_of_right_ne_nil (s : List α) : t ≠ [] → s ++ t ≠ []

Proof state:
α : Type u_1
t s : List α
⊢ t ≠ [] → s ++ t ≠ []

Tactic:
simp_all

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean
theorem LocalizationMap.sec_zero_fst {f : LocalizationMap S N} : f.toMap (f.sec 0).fst = 0

Proof state:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoidWithZero N
f : S.LocalizationMap N
⊢ f.toMap (f.sec 0).1 = 0

Tactic:
rw [LocalizationMap.sec_spec', mul_zero]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem edgeSet_sup {H₁ H₂ : Subgraph G} : (H₁ ⊔ H₂).edgeSet = H₁.edgeSet ∪ H₂.edgeSet :=
  Set.ext <| Sym2.ind (by simp)

Proof state:
V : Type u
G : SimpleGraph V
H₁ H₂ : G.Subgraph
⊢ ∀ (x y : V), s(x, y) ∈ (H₁ ⊔ H₂).edgeSet ↔ s(x, y) ∈ H₁.edgeSet ∪ H₂.edgeSet

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem updateCol_apply [DecidableEq n] {j' : n} :
    updateCol M j c i j' = if j' = j then c i else M i j'

Proof state:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'

Tactic:
by_cases h : j' = j

Result:
case pos
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
h : j' = j
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'

case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
h : ¬j' = j
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'

Proof state:
case pos
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
h : j' = j
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'

Tactic:
rw [h, updateCol_self, if_pos rfl]

Result:
no goals

Proof state:
case neg
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
h : ¬j' = j
⊢ M.updateCol j c i j' = if j' = j then c i else M i j'

Tactic:
rw [updateCol_ne h, if_neg h]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
lemma smul_def (m : R) (g : SpecialLinearGroup n R) (A : (FixedDetMatrix n R m)) :
    g • A = ⟨g * A.1, by simp only [det_mul, SpecialLinearGroup.det_coe, A.2, one_mul]⟩ :=
  rfl

Proof state:
n : Type u_1
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type u_2
inst✝ : CommRing R
m : R
g : SpecialLinearGroup n R
A : FixedDetMatrix n R m
⊢ (↑g * ↑A).det = m

Tactic:
simp only [det_mul, SpecialLinearGroup.det_coe, A.2, one_mul]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem _root_.Matrix.posDef_diagonal_iff
    [StarOrderedRing R] [DecidableEq n] [NoZeroDivisors R] [Nontrivial R] {d : n → R} :
    PosDef (diagonal d) ↔ ∀ i, 0 < d i

Proof state:
n : Type u_2
R : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : DecidableEq n
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
d : n → R
h : (diagonal d).PosDef
i : n
this : (∃ a, Pi.single i 1 a ≠ 0 a) → 0 < d i
⊢ 0 < d i

Tactic:
exact this ⟨i, by simp⟩

Result:
no goals

Proof state:
n : Type u_2
R : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : DecidableEq n
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
d : n → R
h : (diagonal d).PosDef
i : n
this : (∃ a, Pi.single i 1 a ≠ 0 a) → 0 < d i
⊢ Pi.single i 1 i ≠ 0 i

Tactic:
simp

Result:
no goals

Proof state:
n : Type u_2
R : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : DecidableEq n
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
d : n → R
h : (diagonal d).PosDef
i : n
this : Pi.single i 1 ≠ 0 → 0 < star (Pi.single i 1) ⬝ᵥ diagonal d *ᵥ Pi.single i 1
⊢ 0 < d i

Tactic:
simp_rw [mulVec_single_one, ← Pi.single_star, star_one, single_dotProduct, one_mul,
  transpose_apply, diagonal_apply_eq, Function.ne_iff] at this

Result:
n : Type u_2
R : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : DecidableEq n
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
d : n → R
h : (diagonal d).PosDef
i : n
this : (∃ a, Pi.single i 1 a ≠ 0 a) → 0 < d i
⊢ 0 < d i

Proof state:
n : Type u_2
R : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : DecidableEq n
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
d : n → R
⊢ (diagonal d).PosDef ↔ ∀ (i : n), 0 < d i

Tactic:
refine ⟨fun h i => ?_, .diagonal⟩

Result:
n : Type u_2
R : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : DecidableEq n
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
d : n → R
h : (diagonal d).PosDef
i : n
⊢ 0 < d i

Proof state:
n : Type u_2
R : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : DecidableEq n
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
d : n → R
h : (diagonal d).PosDef
i : n
⊢ 0 < d i

Tactic:
have := h.2 (Pi.single i 1)

Result:
n : Type u_2
R : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : CommRing R
inst✝⁵ : PartialOrder R
inst✝⁴ : StarRing R
inst✝³ : StarOrderedRing R
inst✝² : DecidableEq n
inst✝¹ : NoZeroDivisors R
inst✝ : Nontrivial R
d : n → R
h : (diagonal d).PosDef
i : n
this : Pi.single i 1 ≠ 0 → 0 < star (Pi.single i 1) ⬝ᵥ diagonal d *ᵥ Pi.single i 1
⊢ 0 < d i