harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_sub_distrib (s : Finset ι) (f g : ι → M) :
    𝔼 i ∈ s, (f i - g i) = 𝔼 i ∈ s, f i - 𝔼 i ∈ s, g i

Proof state:
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module ℚ≥0 M
s : Finset ι
f g : ι → M
⊢ 𝔼 i ∈ s, (f i - g i) = 𝔼 i ∈ s, f i - 𝔼 i ∈ s, g i

Tactic:
simp only [expect, sum_sub_distrib, smul_sub]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem degreeOf_add_le (n : σ) (f g : MvPolynomial σ R) :
    degreeOf n (f + g) ≤ max (degreeOf n f) (degreeOf n g)

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f g : MvPolynomial σ R
⊢ ((f + g).support.sup fun m => m n) ≤ (f.support.sup fun m => m n) ⊔ g.support.sup fun m => m n

Tactic:
exact supDegree_add_le

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f g : MvPolynomial σ R
⊢ degreeOf n (f + g) ≤ degreeOf n f ⊔ degreeOf n g

Tactic:
simp_rw [degreeOf_eq_sup]

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
n : σ
f g : MvPolynomial σ R
⊢ ((f + g).support.sup fun m => m n) ≤ (f.support.sup fun m => m n) ⊔ g.support.sup fun m => m n
-- Mathlib/Algebra/MonoidAlgebra/Support.lean
theorem support_single_mul_subset [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) (r : k) (a : G) :
    (single a r * f : MonoidAlgebra k G).support ⊆ Finset.image (a * ·) f.support :=
  (support_mul _ _).trans <| (Finset.image₂_subset_right support_single_subset).trans <| by
    rw [Finset.image₂_singleton_left]

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : DecidableEq G
inst✝ : Mul G
f : MonoidAlgebra k G
r : k
a : G
⊢ image₂ (fun x1 x2 => x1 * x2) {a} f.support ⊆ image (fun x => a * x) f.support

Tactic:
rw [Finset.image₂_singleton_left]

Result:
no goals
-- Mathlib/Tactic/NormNum/Basic.lean
theorem isintCast {R} [Ring R] (n m : ℤ) :
    IsInt n m → IsInt (n : R) m

Proof state:
case mk.refl
R : Type u_1
inst✝ : Ring R
m : ℤ
⊢ IsInt (↑↑m) m

Tactic:
exact ⟨rfl⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
n m : ℤ
⊢ IsInt n m → IsInt (↑n) m

Tactic:
rintro ⟨⟨⟩⟩

Result:
case mk.refl
R : Type u_1
inst✝ : Ring R
m : ℤ
⊢ IsInt (↑↑m) m
-- Mathlib/NumberTheory/DiophantineApproximation/ContinuedFractions.lean
theorem convs_eq_convergent (ξ : ℝ) (n : ℕ) :
    (GenContFract.of ξ).convs n = ξ.convergent n

Proof state:
ξ : ℝ
n : ℕ
⊢ (GenContFract.of ξ).convs n = ↑(ξ.convergent n)

Tactic:
induction n generalizing ξ with
| zero => simp only [zeroth_conv_eq_h, of_h_eq_floor, convergent_zero, Rat.cast_intCast]
| succ n ih => rw [convs_succ, ih (fract ξ)⁻¹, convergent_succ, one_div]; norm_cast

Result:
no goals

Proof state:
case zero
ξ : ℝ
⊢ (GenContFract.of ξ).convs 0 = ↑(ξ.convergent 0)

Tactic:
simp only [zeroth_conv_eq_h, of_h_eq_floor, convergent_zero, Rat.cast_intCast]

Result:
no goals

Proof state:
case succ
n : ℕ
ih : ∀ (ξ : ℝ), (GenContFract.of ξ).convs n = ↑(ξ.convergent n)
ξ : ℝ
⊢ ↑⌊ξ⌋ + (↑((fract ξ)⁻¹.convergent n))⁻¹ = ↑(↑⌊ξ⌋ + ((fract ξ)⁻¹.convergent n)⁻¹)

Tactic:
norm_cast

Result:
no goals

Proof state:
case succ
n : ℕ
ih : ∀ (ξ : ℝ), (GenContFract.of ξ).convs n = ↑(ξ.convergent n)
ξ : ℝ
⊢ (GenContFract.of ξ).convs (n + 1) = ↑(ξ.convergent (n + 1))

Tactic:
rw [convs_succ, ih (fract ξ)⁻¹, convergent_succ, one_div]

Result:
case succ
n : ℕ
ih : ∀ (ξ : ℝ), (GenContFract.of ξ).convs n = ↑(ξ.convergent n)
ξ : ℝ
⊢ ↑⌊ξ⌋ + (↑((fract ξ)⁻¹.convergent n))⁻¹ = ↑(↑⌊ξ⌋ + ((fract ξ)⁻¹.convergent n)⁻¹)
-- Mathlib/Topology/StoneCech.lean
theorem ultrafilter_isClosed_basic (s : Set α) : IsClosed { u : Ultrafilter α | s ∈ u }

Proof state:
case h.e'_3
α : Type u
s : Set α
⊢ {u | s ∈ u}ᶜ = {u | sᶜ ∈ u}

Tactic:
ext u

Result:
case h.e'_3.h
α : Type u
s : Set α
u : Ultrafilter α
⊢ u ∈ {u | s ∈ u}ᶜ ↔ u ∈ {u | sᶜ ∈ u}

Proof state:
α : Type u
s : Set α
⊢ IsOpen {u | s ∈ u}ᶜ

Tactic:
convert ultrafilter_isOpen_basic sᶜ using 1

Result:
case h.e'_3
α : Type u
s : Set α
⊢ {u | s ∈ u}ᶜ = {u | sᶜ ∈ u}

Proof state:
case h.e'_3.h
α : Type u
s : Set α
u : Ultrafilter α
⊢ u ∈ {u | s ∈ u}ᶜ ↔ u ∈ {u | sᶜ ∈ u}

Tactic:
exact Ultrafilter.compl_mem_iff_not_mem.symm

Result:
no goals

Proof state:
α : Type u
s : Set α
⊢ IsClosed {u | s ∈ u}

Tactic:
rw [← isOpen_compl_iff]

Result:
α : Type u
s : Set α
⊢ IsOpen {u | s ∈ u}ᶜ
-- Mathlib/Order/Filter/SmallSets.lean
theorem smallSets_top : (⊤ : Filter α).smallSets = ⊤

Proof state:
α : Type u_1
⊢ ⊤.smallSets = ⊤

Tactic:
rw [smallSets, lift'_top, powerset_univ, principal_univ]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_sub_natCast {x : ℝ} (hx : x ≠ 0) (y : ℝ) (n : ℕ) : x ^ (y - n) = x ^ y / x ^ n

Proof state:
x : ℝ
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y - ↑n) = x ^ y / x ^ n

Tactic:
simpa using rpow_sub_intCast hx y n

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurable_find {p : α → ℕ → Prop} [∀ x, DecidablePred (p x)] (hp : ∀ x, ∃ N, p x N)
    (hm : ∀ k, MeasurableSet { x | p x k }) : Measurable fun x => Nat.find (hp x)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ N, p x N
hm : ∀ (k : ℕ), MeasurableSet {x | p x k}
⊢ Measurable fun x => Nat.find ⋯

Tactic:
refine measurable_to_nat fun x => ?_

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ N, p x N
hm : ∀ (k : ℕ), MeasurableSet {x | p x k}
x : α
⊢ MeasurableSet ((fun x => Nat.find ⋯) ⁻¹' {Nat.find ⋯})

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ N, p x N
hm : ∀ (k : ℕ), MeasurableSet {x | p x k}
x : α
⊢ MeasurableSet (disjointed (fun k => {x | p x k}) (Nat.find ⋯))

Tactic:
exact MeasurableSet.disjointed hm _

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ N, p x N
hm : ∀ (k : ℕ), MeasurableSet {x | p x k}
x : α
⊢ MeasurableSet ((fun x => Nat.find ⋯) ⁻¹' {Nat.find ⋯})

Tactic:
rw [preimage_find_eq_disjointed (fun k => {x | p x k})]

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
p : α → ℕ → Prop
inst✝ : (x : α) → DecidablePred (p x)
hp : ∀ (x : α), ∃ N, p x N
hm : ∀ (k : ℕ), MeasurableSet {x | p x k}
x : α
⊢ MeasurableSet (disjointed (fun k => {x | p x k}) (Nat.find ⋯))
-- Mathlib/Order/OrderIsoNat.lean
theorem wellFounded_iff_no_descending_seq :
    WellFounded r ↔ IsEmpty (((· > ·) : ℕ → ℕ → Prop) ↪r r)

Proof state:
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
⊢ WellFounded r ↔ IsEmpty ((fun x1 x2 => x1 > x2) ↪r r)

Tactic:
constructor

Result:
case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
⊢ WellFounded r → IsEmpty ((fun x1 x2 => x1 > x2) ↪r r)

case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
⊢ IsEmpty ((fun x1 x2 => x1 > x2) ↪r r) → WellFounded r

Proof state:
case mp.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
h : ∀ (a : α), Acc r a
⊢ IsEmpty ((fun x1 x2 => x1 > x2) ↪r r)

Tactic:
exact ⟨fun f => not_acc_of_decreasing_seq f 0 (h _)⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
h : IsEmpty ((fun x1 x2 => x1 > x2) ↪r r)
⊢ WellFounded r

Tactic:
exact ⟨fun x => acc_iff_no_decreasing_seq.2 inferInstance⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
⊢ IsEmpty ((fun x1 x2 => x1 > x2) ↪r r) → WellFounded r

Tactic:
intro h

Result:
case mpr
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
h : IsEmpty ((fun x1 x2 => x1 > x2) ↪r r)
⊢ WellFounded r

Proof state:
case mp
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
⊢ WellFounded r → IsEmpty ((fun x1 x2 => x1 > x2) ↪r r)

Tactic:
rintro ⟨h⟩

Result:
case mp.intro
α : Type u_1
r : α → α → Prop
inst✝ : IsStrictOrder α r
h : ∀ (a : α), Acc r a
⊢ IsEmpty ((fun x1 x2 => x1 > x2) ↪r r)
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem exists_SL2_smul_eq_of_apply_zero_one_eq_zero (g : SL(2, ℝ)) (hc : g 1 0 = 0) :
    ∃ (u : { x : ℝ // 0 < x }) (v : ℝ), (g • · : ℍ → ℍ) = (v +ᵥ ·) ∘ (u • ·)

Proof state:
case intro.intro.intro
a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
⊢ (fun x => ⟨!![a, b; 0, a⁻¹], ⋯⟩ • x) = (fun x => b * a +ᵥ x) ∘ fun x => ⟨a * a, ⋯⟩ • x

Tactic:
ext1 ⟨z, hz⟩

Result:
case intro.intro.intro.h.mk
a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
z : ℂ
hz : 0 < z.im
⊢ ⟨!![a, b; 0, a⁻¹], ⋯⟩ • ⟨z, hz⟩ = ((fun x => b * a +ᵥ x) ∘ fun x => ⟨a * a, ⋯⟩ • x) ⟨z, hz⟩

Proof state:
a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
z : ℂ
hz : 0 < z.im
this : ↑a * z * ↑a + ↑b * ↑a = ↑b * ↑a + ↑a * ↑a * z
⊢ ↑(⟨!![a, b; 0, a⁻¹], ⋯⟩ • ⟨z, hz⟩) = ↑(((fun x => b * a +ᵥ x) ∘ fun x => ⟨a * a, ⋯⟩ • x) ⟨z, hz⟩)

Tactic:
simpa [toGL, specialLinearGroup_apply, add_mul]

Result:
no goals

Proof state:
case intro.intro.intro.h.mk.h
a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
z : ℂ
hz : 0 < z.im
⊢ ↑(⟨!![a, b; 0, a⁻¹], ⋯⟩ • ⟨z, hz⟩) = ↑(((fun x => b * a +ᵥ x) ∘ fun x => ⟨a * a, ⋯⟩ • x) ⟨z, hz⟩)

Tactic:
suffices ↑a * z * a + b * a = b * a + a * a * z by
  simpa [toGL, specialLinearGroup_apply, add_mul]

Result:
case intro.intro.intro.h.mk.h
a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
z : ℂ
hz : 0 < z.im
⊢ ↑a * z * ↑a + ↑b * ↑a = ↑b * ↑a + ↑a * ↑a * z

Proof state:
case intro.intro.intro
a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
⊢ ∃ u v, (fun x => ⟨!![a, b; 0, a⁻¹], ⋯⟩ • x) = (fun x => v +ᵥ x) ∘ fun x => u • x

Tactic:
refine ⟨⟨_, mul_self_pos.mpr ha⟩, b * a, ?_⟩

Result:
case intro.intro.intro
a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
⊢ (fun x => ⟨!![a, b; 0, a⁻¹], ⋯⟩ • x) = (fun x => b * a +ᵥ x) ∘ fun x => ⟨a * a, ⋯⟩ • x

Proof state:
case intro.intro.intro.h.mk.h
a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
z : ℂ
hz : 0 < z.im
⊢ ↑a * z * ↑a + ↑b * ↑a = ↑b * ↑a + ↑a * ↑a * z

Tactic:
ring

Result:
no goals

Proof state:
g : SL(2, ℝ)
hc : ↑g 1 0 = 0
⊢ ∃ u v, (fun x => g • x) = (fun x => v +ᵥ x) ∘ fun x => u • x

Tactic:
obtain ⟨a, b, ha, rfl⟩ := g.fin_two_exists_eq_mk_of_apply_zero_one_eq_zero hc

Result:
case intro.intro.intro
a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
⊢ ∃ u v, (fun x => ⟨!![a, b; 0, a⁻¹], ⋯⟩ • x) = (fun x => v +ᵥ x) ∘ fun x => u • x

Proof state:
case intro.intro.intro.h.mk
a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
z : ℂ
hz : 0 < z.im
⊢ ⟨!![a, b; 0, a⁻¹], ⋯⟩ • ⟨z, hz⟩ = ((fun x => b * a +ᵥ x) ∘ fun x => ⟨a * a, ⋯⟩ • x) ⟨z, hz⟩

Tactic:
ext1

Result:
case intro.intro.intro.h.mk.h
a b : ℝ
ha : a ≠ 0
hc : ↑⟨!![a, b; 0, a⁻¹], ⋯⟩ 1 0 = 0
z : ℂ
hz : 0 < z.im
⊢ ↑(⟨!![a, b; 0, a⁻¹], ⋯⟩ • ⟨z, hz⟩) = ↑(((fun x => b * a +ᵥ x) ∘ fun x => ⟨a * a, ⋯⟩ • x) ⟨z, hz⟩)
-- Mathlib/Algebra/Lie/Submodule.lean
theorem comap_incl_eq_top : N₂.comap N.incl = ⊤ ↔ N ≤ N₂

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N N₂ : LieSubmodule R L M
⊢ comap N.incl N₂ = ⊤ ↔ N ≤ N₂

Tactic:
rw [← LieSubmodule.toSubmodule_inj, LieSubmodule.toSubmodule_comap, LieSubmodule.incl_coe,
  LieSubmodule.top_toSubmodule, Submodule.comap_subtype_eq_top, toSubmodule_le_toSubmodule]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
theorem isPerfectMatching_iff_forall_degree [∀ v, Fintype (M.neighborSet v)] :
    M.IsPerfectMatching ↔ ∀ v, M.degree v = 1

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
inst✝ : (v : V) → Fintype ↑(M.neighborSet v)
⊢ M.IsPerfectMatching ↔ ∀ (v : V), M.degree v = 1

Tactic:
simp [degree_eq_one_iff_unique_adj, isPerfectMatching_iff]

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem preimage_coe_Icc : (some : α → WithTop α) ⁻¹' Icc a b = Icc a b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ some ⁻¹' Icc ↑a ↑b = Icc a b

Tactic:
simp [← Ici_inter_Iic]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Ring.lean
theorem ofPow {i} (a : A i) (n : ℕ) :
    of _ i a ^ n = of _ (n • i) (GradedMonoid.GMonoid.gnpow _ a)

Proof state:
case zero
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
⊢ (of A i) a ^ 0 = (of A (0 • i)) (GradedMonoid.GMonoid.gnpow 0 a)

Tactic:
exact of_eq_of_gradedMonoid_eq (pow_zero <| GradedMonoid.mk _ a).symm

Result:
no goals

Proof state:
case succ
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
n_ih : (of A i) a ^ n = (of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
⊢ (of A (n • i + i)) (GradedMonoid.GMul.mul (GradedMonoid.GMonoid.gnpow n a) a) =
    (of A ((n + 1) • i)) (GradedMonoid.GMonoid.gnpow (n + 1) a)

Tactic:
exact of_eq_of_gradedMonoid_eq (pow_succ (GradedMonoid.mk _ a) n).symm

Result:
no goals

Proof state:
case succ
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
n_ih : (of A i) a ^ n = (of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
⊢ (of A i) a ^ (n + 1) = (of A ((n + 1) • i)) (GradedMonoid.GMonoid.gnpow (n + 1) a)

Tactic:
rw [pow_succ, n_ih, of_mul_of]

Result:
case succ
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
n_ih : (of A i) a ^ n = (of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)
⊢ (of A (n • i + i)) (GradedMonoid.GMul.mul (GradedMonoid.GMonoid.gnpow n a) a) =
    (of A ((n + 1) • i)) (GradedMonoid.GMonoid.gnpow (n + 1) a)

Proof state:
ι : Type u_1
inst✝³ : DecidableEq ι
A : ι → Type u_2
inst✝² : (i : ι) → AddCommMonoid (A i)
inst✝¹ : AddMonoid ι
inst✝ : GSemiring A
i : ι
a : A i
n : ℕ
⊢ (of A i) a ^ n = (of A (n • i)) (GradedMonoid.GMonoid.gnpow n a)

Tactic:
induction n with
| zero => exact of_eq_of_gradedMonoid_eq (pow_zero <| GradedMonoid.mk _ a).symm
| succ n n_ih =>
  rw [pow_succ, n_ih, of_mul_of]
  exact of_eq_of_gradedMonoid_eq (pow_succ (GradedMonoid.mk _ a) n).symm

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
lemma iInf_coe_eq_top : ⨅ x, (f x : WithTop α) = ⊤ ↔ IsEmpty ι

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
f : ι → α
⊢ ⨅ x, ↑(f x) = ⊤ ↔ IsEmpty ι

Tactic:
simp [isEmpty_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem Matrix.toLin_toMatrix (f : M₁ →ₗ[R] M₂) :
    Matrix.toLin v₁ v₂ (LinearMap.toMatrix v₁ v₂ f) = f

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
⊢ (toLin v₁ v₂) ((toMatrix v₁ v₂) f) = f

Tactic:
rw [← Matrix.toLin_symm, LinearEquiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem mul_const (hm : IsPeriodicPt f m x) (n : ℕ) : IsPeriodicPt f (m * n) x

Proof state:
α : Type u_1
f : α → α
x : α
m : ℕ
hm : IsPeriodicPt f m x
n : ℕ
⊢ IsPeriodicPt f (m * n) x

Tactic:
simp only [IsPeriodicPt, iterate_mul, hm.isFixedPt.iterate n]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.ro_eq_true_of_lo (u v k₁ k₂ : Nat) : u + k₁ ≤ v → (u ≤ v + k₂) = True :=
  by simp; omega

Proof state:
u v k₁ k₂ : Nat
⊢ u + k₁ ≤ v → u ≤ v + k₂

Tactic:
omega

Result:
no goals

Proof state:
u v k₁ k₂ : Nat
⊢ u + k₁ ≤ v → (u ≤ v + k₂) = True

Tactic:
simp

Result:
u v k₁ k₂ : Nat
⊢ u + k₁ ≤ v → u ≤ v + k₂
-- Mathlib/Data/Num/Lemmas.lean
theorem zneg_pred (n : ZNum) : -n.pred = (-n).succ

Proof state:
n : ZNum
⊢ -n.pred = (-n).succ

Tactic:
rw [← zneg_zneg (succ (-n)), zneg_succ, zneg_zneg]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem eq_of_norm_div_le_zero (h : ‖a / b‖ ≤ 0) : a = b

Proof state:
E : Type u_5
inst✝ : NormedGroup E
a b : E
h : ‖a / b‖ ≤ 0
⊢ a = b

Tactic:
rwa [← div_eq_one, ← norm_le_zero_iff']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_insertManyIfNewUnit_empty_list
    {l : List α} {k : α} {fallback : Unit} :
    getD (insertManyIfNewUnit (empty : Raw₀ α (fun _ => Unit)) l) k fallback = ()

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
l : List α
k : α
fallback : Unit
⊢ getD (insertManyIfNewUnit empty l).val k fallback = ()

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Star/Subalgebra.lean
theorem top_toSubalgebra : (⊤ : StarSubalgebra R A).toSubalgebra = ⊤

Proof state:
case h
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
x✝ : A
⊢ x✝ ∈ ⊤.toSubalgebra ↔ x✝ ∈ ⊤

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
⊢ ⊤.toSubalgebra = ⊤

Tactic:
ext

Result:
case h
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
x✝ : A
⊢ x✝ ∈ ⊤.toSubalgebra ↔ x✝ ∈ ⊤
-- Mathlib/Algebra/BigOperators/Expect.lean
/-- Reorder an average.

The difference with `Finset.expect_nbij` is that the bijection is specified with an inverse, rather
than as a surjective injection.

The difference with `Finset.expect_bij'` is that the bijection and its inverse are non-dependent
functions, rather than being allowed to use membership of the domains of the averages.

The difference with `Finset.expect_equiv` is that bijectivity is only required to hold on the
domains of the averages, rather than on the entire types. -/
lemma expect_nbij' (i : ι → κ) (j : κ → ι) (hi : ∀ a ∈ s, i a ∈ t) (hj : ∀ a ∈ t, j a ∈ s)
    (left_inv : ∀ a ∈ s, j (i a) = a) (right_inv : ∀ a ∈ t, i (j a) = a)
    (h : ∀ a ∈ s, f a = g (i a)) : 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Proof state:
ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f : ι → M
t : Finset κ
g : κ → M
i : ι → κ
j : κ → ι
hi : ∀ a ∈ s, i a ∈ t
hj : ∀ a ∈ t, j a ∈ s
left_inv : ∀ a ∈ s, j (i a) = a
right_inv : ∀ a ∈ t, i (j a) = a
h : ∀ a ∈ s, f a = g (i a)
⊢ 𝔼 i ∈ s, f i = 𝔼 i ∈ t, g i

Tactic:
simp_rw [expect, card_nbij' i j hi hj left_inv right_inv,
  sum_nbij' i j hi hj left_inv right_inv h]

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem rank_zero_iff_forall_zero :
    Module.rank R M = 0 ↔ ∀ x : M, x = 0

Proof state:
R : Type u
M : Type v
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Nontrivial R
inst✝ : NoZeroSMulDivisors R M
⊢ Module.rank R M = 0 ↔ ∀ (x : M), x = 0

Tactic:
simp_rw [rank_eq_zero_iff, smul_eq_zero, and_or_left, not_and_self_iff, false_or,
  exists_and_right, and_iff_right (exists_ne (0 : R))]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Group.lean
theorem sub_mem_Ioc_zero_iff_right : b - a ∈ Ioc 0 b ↔ a ∈ Ico 0 b

Proof state:
α : Type u_1
inst✝ : OrderedAddCommGroup α
a b : α
⊢ b - a ∈ Ioc 0 b ↔ a ∈ Ico 0 b

Tactic:
simp only [sub_mem_Ioc_iff_right, sub_self, sub_zero]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
@[to_additive (attr := simp)]
protected lemma div_mul_cancel (h : IsUnit b) (a : α) : a / b * b = a

Proof state:
α : Type u
inst✝ : DivisionMonoid α
b : α
h : IsUnit b
a : α
⊢ a / b * b = a

Tactic:
rw [div_eq_mul_inv, h.inv_mul_cancel_right]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem tensor_associativity (X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C) :
    (tensorμ X₁ X₂ Y₁ Y₂ ▷ (Z₁ ⊗ Z₂)) ≫
        tensorμ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) Z₁ Z₂ ≫ ((α_ X₁ Y₁ Z₁).hom ⊗ (α_ X₂ Y₂ Z₂).hom) =
      (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫
        ((X₁ ⊗ X₂) ◁ tensorμ Y₁ Y₂ Z₁ Z₂) ≫ tensorμ X₁ X₂ (Y₁ ⊗ Z₁) (Y₂ ⊗ Z₂)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
⊢ ((α_ X₁ X₂ (Y₁ ⊗ Y₂)).hom ≫
          X₁ ◁ (α_ X₂ Y₁ Y₂).inv ≫ X₁ ◁ (β_ X₂ Y₁).hom ▷ Y₂ ≫ X₁ ◁ (α_ Y₁ X₂ Y₂).hom ≫ (α_ X₁ Y₁ (X₂ ⊗ Y₂)).inv) ▷
        (Z₁ ⊗ Z₂) ≫
      ((α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫
          (X₁ ⊗ Y₁) ◁ (α_ (X₂ ⊗ Y₂) Z₁ Z₂).inv ≫
            (X₁ ⊗ Y₁) ◁
                ((α_ X₂ Y₂ Z₁).hom ≫
                    X₂ ◁ (β_ Y₂ Z₁).hom ≫ (α_ X₂ Z₁ Y₂).inv ≫ (β_ X₂ Z₁).hom ▷ Y₂ ≫ (α_ Z₁ X₂ Y₂).hom) ▷
                  Z₂ ≫
              (X₁ ⊗ Y₁) ◁ (α_ Z₁ (X₂ ⊗ Y₂) Z₂).hom ≫ (α_ (X₁ ⊗ Y₁) Z₁ ((X₂ ⊗ Y₂) ⊗ Z₂)).inv) ≫
        ((α_ X₁ Y₁ Z₁).hom ⊗ (α_ X₂ Y₂ Z₂).hom) =
    𝟙 (((X₁ ⊗ X₂) ⊗ Y₁ ⊗ Y₂) ⊗ Z₁ ⊗ Z₂) ⊗≫
      X₁ ◁ ((β_ X₂ Y₁).hom ▷ (Y₂ ⊗ Z₁) ≫ (Y₁ ⊗ X₂) ◁ (β_ Y₂ Z₁).hom) ▷ Z₂ ⊗≫
        X₁ ◁ Y₁ ◁ (β_ X₂ Z₁).hom ▷ Y₂ ▷ Z₂ ⊗≫ 𝟙 ((X₁ ⊗ Y₁ ⊗ Z₁) ⊗ X₂ ⊗ Y₂ ⊗ Z₂)

Tactic:
monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
⊢ 𝟙 (((X₁ ⊗ X₂) ⊗ Y₁ ⊗ Y₂) ⊗ Z₁ ⊗ Z₂) ⊗≫
      X₁ ◁ ((X₂ ⊗ Y₁) ◁ (β_ Y₂ Z₁).hom ≫ (β_ X₂ Y₁).hom ▷ (Z₁ ⊗ Y₂)) ▷ Z₂ ⊗≫
        X₁ ◁ Y₁ ◁ (β_ X₂ Z₁).hom ▷ Y₂ ▷ Z₂ ⊗≫ 𝟙 ((X₁ ⊗ Y₁ ⊗ Z₁) ⊗ X₂ ⊗ Y₂ ⊗ Z₂) =
    (α_ (X₁ ⊗ X₂) (Y₁ ⊗ Y₂) (Z₁ ⊗ Z₂)).hom ≫
      (X₁ ⊗ X₂) ◁
          ((α_ Y₁ Y₂ (Z₁ ⊗ Z₂)).hom ≫
            Y₁ ◁ (α_ Y₂ Z₁ Z₂).inv ≫ Y₁ ◁ (β_ Y₂ Z₁).hom ▷ Z₂ ≫ Y₁ ◁ (α_ Z₁ Y₂ Z₂).hom ≫ (α_ Y₁ Z₁ (Y₂ ⊗ Z₂)).inv) ≫
        (α_ X₁ X₂ ((Y₁ ⊗ Z₁) ⊗ Y₂ ⊗ Z₂)).hom ≫
          X₁ ◁ (α_ X₂ (Y₁ ⊗ Z₁) (Y₂ ⊗ Z₂)).inv ≫
            X₁ ◁
                ((α_ X₂ Y₁ Z₁).inv ≫
                    (β_ X₂ Y₁).hom ▷ Z₁ ≫ (α_ Y₁ X₂ Z₁).hom ≫ Y₁ ◁ (β_ X₂ Z₁).hom ≫ (α_ Y₁ Z₁ X₂).inv) ▷
                  (Y₂ ⊗ Z₂) ≫
              X₁ ◁ (α_ (Y₁ ⊗ Z₁) X₂ (Y₂ ⊗ Z₂)).hom ≫ (α_ X₁ (Y₁ ⊗ Z₁) (X₂ ⊗ Y₂ ⊗ Z₂)).inv

Tactic:
monoidal

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Lipschitz.lean
theorem prod_mk_right (b : β) : LipschitzWith 1 fun a : α => (a, b)

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
b : β
⊢ LipschitzWith 1 fun a => (a, b)

Tactic:
simpa only [max_eq_left zero_le_one] using LipschitzWith.id.prod (LipschitzWith.const b)

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Defs.lean
theorem mul_ne_zero_iff_left (ha : a ≠ 0) : a * b ≠ 0 ↔ b ≠ 0

Proof state:
M₀ : Type u_1
inst✝¹ : MulZeroClass M₀
inst✝ : NoZeroDivisors M₀
a b : M₀
ha : a ≠ 0
⊢ a * b ≠ 0 ↔ b ≠ 0

Tactic:
simp [ha]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem iSup₂_comm {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*}
    (f : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → α) :
    ⨆ (i₁) (j₁) (i₂) (j₂), f i₁ j₁ i₂ j₂ = ⨆ (i₂) (j₂) (i₁) (j₁), f i₁ j₁ i₂ j₂

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
ι₁ : Sort u_8
ι₂ : Sort u_9
κ₁ : ι₁ → Sort u_10
κ₂ : ι₂ → Sort u_11
f : (i₁ : ι₁) → κ₁ i₁ → (i₂ : ι₂) → κ₂ i₂ → α
⊢ ⨆ i₁, ⨆ j₁, ⨆ i₂, ⨆ j₂, f i₁ j₁ i₂ j₂ = ⨆ i₂, ⨆ j₂, ⨆ i₁, ⨆ j₁, f i₁ j₁ i₂ j₂

Tactic:
simp only [@iSup_comm _ (κ₁ _), @iSup_comm _ ι₁]

Result:
no goals