harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem foldlM_toArray' [Monad m] (f : β → α → m β) (init : β) (l : List α)
    (h : stop = l.toArray.size) :
    l.toArray.foldlM f init 0 stop = l.foldlM f init

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
stop : Nat
inst✝ : Monad m
f : β → α → m β
init : β
l : List α
h : stop = l.toArray.size
⊢ foldlM f init l.toArray 0 stop = List.foldlM f init l

Tactic:
subst h

Result:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
init : β
l : List α
⊢ foldlM f init l.toArray = List.foldlM f init l

Proof state:
m : Type u_1 → Type u_2
β : Type u_1
α : Type u_3
inst✝ : Monad m
f : β → α → m β
init : β
l : List α
⊢ foldlM f init l.toArray = List.foldlM f init l

Tactic:
rw [foldlM_toList]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem isCoprime_num_denom (x : RatFunc K) : IsCoprime x.num x.denom

Proof state:
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ IsCoprime (C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)) (C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q))

Tactic:
exact (isCoprime_mul_unit_left
  ((leadingCoeff_ne_zero.2 <| right_div_gcd_ne_zero hq).isUnit.inv.map C) _ _).2
    (isCoprime_div_gcd_div_gcd hq)

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
x : RatFunc K
⊢ IsCoprime x.num x.denom

Tactic:
induction' x using RatFunc.induction_on with p q hq

Result:
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ IsCoprime ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num
    ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).denom

Proof state:
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ IsCoprime ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).num
    ((algebraMap K[X] (RatFunc K)) p / (algebraMap K[X] (RatFunc K)) q).denom

Tactic:
rw [num_div, denom_div _ hq]

Result:
case f
K : Type u
inst✝ : Field K
p q : K[X]
hq : q ≠ 0
⊢ IsCoprime (C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)) (C (q / gcd p q).leadingCoeff⁻¹ * (q / gcd p q))

Proof state:
K : Type u
inst✝ : Field K
x : RatFunc K
⊢ IsCoprime x.num x.denom

Tactic:
classical
induction' x using RatFunc.induction_on with p q hq
rw [num_div, denom_div _ hq]
exact (isCoprime_mul_unit_left
  ((leadingCoeff_ne_zero.2 <| right_div_gcd_ne_zero hq).isUnit.inv.map C) _ _).2
    (isCoprime_div_gcd_div_gcd hq)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem reverse_inj {xs ys : Vector α n} : xs.reverse = ys.reverse ↔ xs = ys

Proof state:
α : Type u_1
n : Nat
xs ys : Vector α n
⊢ xs.reverse = ys.reverse ↔ xs = ys

Tactic:
simp [reverse_eq_iff]

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
@[simp]
lemma integralCLM_apply (f : 𝓢(D, V)) : integralCLM 𝕜 μ f = ∫ x, f x ∂μ

Proof state:
𝕜 : Type u_1
D : Type u_3
V : Type u_7
inst✝⁸ : RCLike 𝕜
inst✝⁷ : NormedAddCommGroup D
inst✝⁶ : NormedSpace ℝ D
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : NormedSpace ℝ V
inst✝³ : NormedSpace 𝕜 V
inst✝² : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
inst✝¹ : BorelSpace D
inst✝ : SecondCountableTopology D
f : 𝓢(D, V)
⊢ (integralCLM 𝕜 μ) f = ∫ (x : D), f x ∂μ

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_eq_sum_div_card (s : Finset ι) (f : ι → M) :
    𝔼 i ∈ s, f i = (∑ i ∈ s, f i) / #s

Proof state:
ι : Type u_1
M : Type u_3
inst✝¹ : Semifield M
inst✝ : CharZero M
s : Finset ι
f : ι → M
⊢ 𝔼 i ∈ s, f i = (∑ i ∈ s, f i) / ↑(#s)

Tactic:
rw [expect, NNRat.smul_def, div_eq_inv_mul, NNRat.cast_inv, NNRat.cast_natCast]

Result:
no goals
-- Mathlib/Control/Bitraversable/Lemmas.lean
theorem comp_tfst {α₀ α₁ α₂ β} (f : α₀ → F α₁) (f' : α₁ → G α₂) (x : t α₀ β) :
    Comp.mk (tfst f' <$> tfst f x) = tfst (Comp.mk ∘ map f' ∘ f) x

Proof state:
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ α₂ β : Type u
f : α₀ → F α₁
f' : α₁ → G α₂
x : t α₀ β
⊢ bitraverse (Comp.mk ∘ map f' ∘ f) (Comp.mk ∘ map pure ∘ pure) x = tfst (Comp.mk ∘ map f' ∘ f) x

Tactic:
simp only [Function.comp_def, tfst, map_pure, Pure.pure]

Result:
no goals

Proof state:
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ α₂ β : Type u
f : α₀ → F α₁
f' : α₁ → G α₂
x : t α₀ β
⊢ Comp.mk (tfst f' <$> tfst f x) = tfst (Comp.mk ∘ map f' ∘ f) x

Tactic:
rw [← comp_bitraverse]

Result:
t : Type u → Type u → Type u
inst✝⁵ : Bitraversable t
F G : Type u → Type u
inst✝⁴ : Applicative F
inst✝³ : Applicative G
inst✝² : LawfulBitraversable t
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α₀ α₁ α₂ β : Type u
f : α₀ → F α₁
f' : α₁ → G α₂
x : t α₀ β
⊢ bitraverse (Comp.mk ∘ map f' ∘ f) (Comp.mk ∘ map pure ∘ pure) x = tfst (Comp.mk ∘ map f' ∘ f) x
-- Mathlib/LinearAlgebra/Matrix/Swap.lean
@[simp]
lemma map_swap (i j : n) : (swap R i j).map f = swap S i j

Proof state:
R : Type u_1
n : Type u_2
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype n
S : Type u_3
inst✝ : CommRing S
f : R →+* S
i j : n
⊢ (map f) (swap R i j) = swap S i j

Tactic:
ext : 1

Result:
case a
R : Type u_1
n : Type u_2
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype n
S : Type u_3
inst✝ : CommRing S
f : R →+* S
i j : n
⊢ ↑((map f) (swap R i j)) = ↑(swap S i j)

Proof state:
case a
R : Type u_1
n : Type u_2
inst✝³ : CommRing R
inst✝² : DecidableEq n
inst✝¹ : Fintype n
S : Type u_3
inst✝ : CommRing S
f : R →+* S
i j : n
⊢ ↑((map f) (swap R i j)) = ↑(swap S i j)

Tactic:
simp [swap]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem eq_nat_or_omega0_le (o : Ordinal) : (∃ n : ℕ, o = n) ∨ ω ≤ o

Proof state:
o : Ordinal.{u_1}
⊢ (∃ n, o = ↑n) ∨ ω ≤ o

Tactic:
obtain ho | ho := lt_or_le o ω

Result:
case inl
o : Ordinal.{u_1}
ho : o < ω
⊢ (∃ n, o = ↑n) ∨ ω ≤ o

case inr
o : Ordinal.{u_1}
ho : ω ≤ o
⊢ (∃ n, o = ↑n) ∨ ω ≤ o

Proof state:
case inr
o : Ordinal.{u_1}
ho : ω ≤ o
⊢ (∃ n, o = ↑n) ∨ ω ≤ o

Tactic:
exact Or.inr ho

Result:
no goals

Proof state:
case inl
o : Ordinal.{u_1}
ho : o < ω
⊢ (∃ n, o = ↑n) ∨ ω ≤ o

Tactic:
exact Or.inl <| lt_omega0.1 ho

Result:
no goals
-- Mathlib/Data/Finset/Powerset.lean
theorem mem_powerset {s t : Finset α} : s ∈ powerset t ↔ s ⊆ t

Proof state:
case mk
α : Type u_1
t : Finset α
val✝ : Multiset α
nodup✝ : val✝.Nodup
⊢ { val := val✝, nodup := nodup✝ } ∈ t.powerset ↔ { val := val✝, nodup := nodup✝ } ⊆ t

Tactic:
simp [powerset, mem_mk, mem_pmap, mk.injEq, mem_powerset, exists_prop, exists_eq_right,
  ← val_le_iff]

Result:
no goals

Proof state:
α : Type u_1
s t : Finset α
⊢ s ∈ t.powerset ↔ s ⊆ t

Tactic:
cases s

Result:
case mk
α : Type u_1
t : Finset α
val✝ : Multiset α
nodup✝ : val✝.Nodup
⊢ { val := val✝, nodup := nodup✝ } ∈ t.powerset ↔ { val := val✝, nodup := nodup✝ } ⊆ t
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_const_add_uIcc : (fun x => a + x) ⁻¹' [[b, c]] = [[b - a, c - a]]

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ (fun x => a + x) ⁻¹' [[b, c]] = [[b - a, c - a]]

Tactic:
simp only [← Icc_min_max, preimage_const_add_Icc, min_sub_sub_right, max_sub_sub_right]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma IsRatCondKernelCDF.mono (hf : IsRatCondKernelCDF f κ ν) (a : α) :
    ∀ᵐ b ∂(ν a), Monotone (f (a, b))

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDF f κ ν
a : α
⊢ ∀ᵐ (b : β) ∂ν a, Monotone (f (a, b))

Tactic:
filter_upwards [hf.isRatStieltjesPoint_ae a] with b hb using hb.mono

Result:
no goals
-- Mathlib/FieldTheory/Laurent.lean
theorem laurent_injective : Function.Injective (laurent r) := fun _ _ h => by
  simpa [laurent_laurent] using congr_arg (laurent (-r)) h

Proof state:
R : Type u
inst✝¹ : CommRing R
r : R
inst✝ : IsDomain R
x✝¹ x✝ : RatFunc R
h : (laurent r) x✝¹ = (laurent r) x✝
⊢ x✝¹ = x✝

Tactic:
simpa [laurent_laurent] using congr_arg (laurent (-r)) h

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem powers_eq_closure (n : M) : powers n = closure {n}

Proof state:
case h
M : Type u_1
inst✝ : Monoid M
n x✝ : M
⊢ x✝ ∈ powers n ↔ x✝ ∈ closure {n}

Tactic:
exact mem_closure_singleton.symm

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
n : M
⊢ powers n = closure {n}

Tactic:
ext

Result:
case h
M : Type u_1
inst✝ : Monoid M
n x✝ : M
⊢ x✝ ∈ powers n ↔ x✝ ∈ closure {n}
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_preimage_mul_left {a : ℝ} (h : a ≠ 0) (s : Set ℝ) :
    volume ((a * ·) ⁻¹' s) = ENNReal.ofReal (abs a⁻¹) * volume s :=
  calc
    volume ((a * ·) ⁻¹' s) = Measure.map (a * ·) volume s :=
      ((Homeomorph.mulLeft₀ a h).toMeasurableEquiv.map_apply s).symm
    _ = ENNReal.ofReal (abs a⁻¹) * volume s

Proof state:
a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ (Measure.map (fun x => a * x) volume) s = ofReal |a⁻¹| * volume s

Tactic:
rw [map_volume_mul_left h]

Result:
a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ (ofReal |a⁻¹| • volume) s = ofReal |a⁻¹| * volume s

Proof state:
a : ℝ
h : a ≠ 0
s : Set ℝ
⊢ (ofReal |a⁻¹| • volume) s = ofReal |a⁻¹| * volume s

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma nonsingular_some (X Y : R) : W'.Nonsingular ![X, Y, 1] ↔ W'.toAffine.Nonsingular X Y

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
X Y : R
⊢ W'.Nonsingular ![X, Y, 1] ↔ (toAffine W').Nonsingular X Y

Tactic:
simp_rw [nonsingular_iff, equation_some, fin3_def_ext, Affine.nonsingular_iff',
  Affine.equation_iff', and_congr_right_iff, ← not_and_or, not_iff_not, one_pow, mul_one,
  and_congr_right_iff, Iff.comm, iff_self_and]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
X Y : R
⊢ Y ^ 2 + (toAffine W').a₁ * X * Y + (toAffine W').a₃ * Y -
        (X ^ 3 + (toAffine W').a₂ * X ^ 2 + (toAffine W').a₄ * X + (toAffine W').a₆) =
      0 →
    W'.a₁ * Y - (3 * X ^ 2 + 2 * W'.a₂ * X + W'.a₄) = 0 →
      2 * Y + (toAffine W').a₁ * X + (toAffine W').a₃ = 0 →
        Y ^ 2 + W'.a₁ * X * Y + 2 * W'.a₃ * Y - (W'.a₂ * X ^ 2 + 2 * W'.a₄ * X + 3 * W'.a₆) = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
X Y : R
h :
  Y ^ 2 + (toAffine W').a₁ * X * Y + (toAffine W').a₃ * Y -
      (X ^ 3 + (toAffine W').a₂ * X ^ 2 + (toAffine W').a₄ * X + (toAffine W').a₆) =
    0
hX : W'.a₁ * Y - (3 * X ^ 2 + 2 * W'.a₂ * X + W'.a₄) = 0
hY : 2 * Y + (toAffine W').a₁ * X + (toAffine W').a₃ = 0
⊢ Y ^ 2 + W'.a₁ * X * Y + 2 * W'.a₃ * Y - (W'.a₂ * X ^ 2 + 2 * W'.a₄ * X + 3 * W'.a₆) = 0

Tactic:
linear_combination (norm := ring1) 3 * h - X * hX - Y * hY

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
X Y : R
⊢ Y ^ 2 + (toAffine W').a₁ * X * Y + (toAffine W').a₃ * Y -
        (X ^ 3 + (toAffine W').a₂ * X ^ 2 + (toAffine W').a₄ * X + (toAffine W').a₆) =
      0 →
    W'.a₁ * Y - (3 * X ^ 2 + 2 * W'.a₂ * X + W'.a₄) = 0 →
      2 * Y + (toAffine W').a₁ * X + (toAffine W').a₃ = 0 →
        Y ^ 2 + W'.a₁ * X * Y + 2 * W'.a₃ * Y - (W'.a₂ * X ^ 2 + 2 * W'.a₄ * X + 3 * W'.a₆) = 0

Tactic:
intro h hX hY

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
X Y : R
h :
  Y ^ 2 + (toAffine W').a₁ * X * Y + (toAffine W').a₃ * Y -
      (X ^ 3 + (toAffine W').a₂ * X ^ 2 + (toAffine W').a₄ * X + (toAffine W').a₆) =
    0
hX : W'.a₁ * Y - (3 * X ^ 2 + 2 * W'.a₂ * X + W'.a₄) = 0
hY : 2 * Y + (toAffine W').a₁ * X + (toAffine W').a₃ = 0
⊢ Y ^ 2 + W'.a₁ * X * Y + 2 * W'.a₃ * Y - (W'.a₂ * X ^ 2 + 2 * W'.a₄ * X + 3 * W'.a₆) = 0
-- Mathlib/Data/List/Basic.lean
theorem map_leftInverse_iff {f : α → β} {g : β → α} :
    LeftInverse (map f) (map g) ↔ LeftInverse f g :=
  ⟨fun h x => by injection h [x], (·.list_map)⟩

Proof state:
α : Type u
β : Type v
f : α → β
g : β → α
h : LeftInverse (map f) (map g)
x : β
⊢ f (g x) = x

Tactic:
injection h [x]

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
lemma Scheme.zeroLocus_iInf
    {X : Scheme.{u}} {U : X.Opens} {ι : Type*}
    (I : ι → Ideal Γ(X, U)) [Finite ι] :
    X.zeroLocus (U := U) ↑(⨅ i, I i) = (⋃ i, X.zeroLocus (U := U) (I i)) ∪ (↑U)ᶜ

Proof state:
X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
inst✝ : Finite ι
⊢ X.zeroLocus ↑(⨅ i, I i) = (⋃ i, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ

Tactic:
simpa using zeroLocus_biInf I Set.finite_univ

Result:
no goals
-- Mathlib/Algebra/Ring/Defs.lean
theorem distrib_three_right [Mul R] [Add R] [RightDistribClass R] (a b c d : R) :
    (a + b + c) * d = a * d + b * d + c * d

Proof state:
R : Type v
inst✝² : Mul R
inst✝¹ : Add R
inst✝ : RightDistribClass R
a b c d : R
⊢ (a + b + c) * d = a * d + b * d + c * d

Tactic:
simp [right_distrib]

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem disjoint_mulSupport_iff {f : α → M} {s : Set α} :
    Disjoint s (mulSupport f) ↔ EqOn f 1 s

Proof state:
α : Type u_1
M : Type u_5
inst✝ : One M
f : α → M
s : Set α
⊢ Disjoint s (mulSupport f) ↔ EqOn f 1 s

Tactic:
rw [disjoint_comm, mulSupport_disjoint_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Subpresheaf/Image.lean
lemma preimage_comp (G : Subpresheaf F) (f : F'' ⟶ F') (g : F' ⟶ F) :
    G.preimage (f ≫ g) = (G.preimage g).preimage f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F F' F'' : Cᵒᵖ ⥤ Type w
G : Subpresheaf F
f : F'' ⟶ F'
g : F' ⟶ F
⊢ G.preimage (f ≫ g) = (G.preimage g).preimage f

Tactic:
aesop

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem lt_top_of_finrank_lt_finrank {s : Submodule R M} (lt : finrank R s < finrank R M) :
    s < ⊤

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
lt : finrank R ↥s < finrank R M
⊢ s < ⊤

Tactic:
rw [← finrank_top R M] at lt

Result:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
lt : finrank R ↥s < finrank R ↥⊤
⊢ s < ⊤

Proof state:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Submodule R M
lt : finrank R ↥s < finrank R ↥⊤
⊢ s < ⊤

Tactic:
exact lt_of_le_of_finrank_lt_finrank le_top lt

Result:
no goals
-- Mathlib/CategoryTheory/Equivalence.lean
theorem inv_fun_map (F : C ⥤ D) [IsEquivalence F] (X Y : C) (f : X ⟶ Y) :
    F.inv.map (F.map f) = F.asEquivalence.unitInv.app X ≫ f ≫ F.asEquivalence.unit.app Y

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
⊢ F.inv.map (F.map f) = (F.asEquivalence.functor ⋙ F.asEquivalence.inverse).map f

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
⊢ F.inv.map (F.map f) = F.asEquivalence.unitInv.app X ≫ f ≫ F.asEquivalence.unit.app Y

Tactic:
erw [NatIso.naturality_1]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : F.IsEquivalence
X Y : C
f : X ⟶ Y
⊢ F.inv.map (F.map f) = (F.asEquivalence.functor ⋙ F.asEquivalence.inverse).map f
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem Basis.toMatrix_reindex' [DecidableEq ι] [DecidableEq ι'] (b : Basis ι R M) (v : ι' → M)
    (e : ι ≃ ι') : (b.reindex e).toMatrix v =
    Matrix.reindexAlgEquiv R R e (b.toMatrix (v ∘ e))

Proof state:
case a
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
i✝ j✝ : ι'
⊢ (b.reindex e).toMatrix v i✝ j✝ = (reindexAlgEquiv R R e) (b.toMatrix (v ∘ ⇑e)) i✝ j✝

Tactic:
simp only [Basis.toMatrix_apply, Basis.repr_reindex, Matrix.reindexAlgEquiv_apply,
  Matrix.reindex_apply, Matrix.submatrix_apply, Function.comp_apply, e.apply_symm_apply,
  Finsupp.mapDomain_equiv_apply]

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
⊢ (b.reindex e).toMatrix v = (reindexAlgEquiv R R e) (b.toMatrix (v ∘ ⇑e))

Tactic:
ext

Result:
case a
ι : Type u_1
ι' : Type u_2
R : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Fintype ι'
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
b : Basis ι R M
v : ι' → M
e : ι ≃ ι'
i✝ j✝ : ι'
⊢ (b.reindex e).toMatrix v i✝ j✝ = (reindexAlgEquiv R R e) (b.toMatrix (v ∘ ⇑e)) i✝ j✝
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem closure_eq_uniformity (s : Set <| α × α) :
    closure s = ⋂ V ∈ { V | V ∈ 𝓤 α ∧ SymmetricRel V }, V ○ s ○ V

Proof state:
case h.mk
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
x y : α
⊢ (x, y) ∈ closure s ↔ (x, y) ∈ ⋂ V ∈ {V | V ∈ 𝓤 α ∧ SymmetricRel V}, V ○ s ○ V

Tactic:
simp +contextual only
  [mem_closure_iff_nhds_basis (UniformSpace.hasBasis_nhds_prod x y), mem_iInter, mem_setOf_eq,
    and_imp, mem_comp_comp, exists_prop, ← mem_inter_iff, inter_comm, Set.Nonempty]

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
⊢ closure s = ⋂ V ∈ {V | V ∈ 𝓤 α ∧ SymmetricRel V}, V ○ s ○ V

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type ua
inst✝ : UniformSpace α
s : Set (α × α)
x y : α
⊢ (x, y) ∈ closure s ↔ (x, y) ∈ ⋂ V ∈ {V | V ∈ 𝓤 α ∧ SymmetricRel V}, V ○ s ○ V
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma comp_assoc_of_first_is_zero_cochain {n₂ n₃ n₂₃ : ℤ}
    (z₁ : Cochain F G 0) (z₂ : Cochain G K n₂) (z₃ : Cochain K L n₃)
    (h₂₃ : n₂ + n₃ = n₂₃) :
    (z₁.comp z₂ (zero_add n₂)).comp z₃ h₂₃ = z₁.comp (z₂.comp z₃ h₂₃) (zero_add n₂₃) :=
  comp_assoc _ _ _ _ _ (by omega)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K L : CochainComplex C ℤ
n₂ n₃ n₂₃ : ℤ
z₁ : Cochain F G 0
z₂ : Cochain G K n₂
z₃ : Cochain K L n₃
h₂₃ : n₂ + n₃ = n₂₃
⊢ 0 + n₂ + n₃ = n₂₃

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Matrix/ColumnRowPartitioned.lean
@[simp]
lemma mul_fromCols [Fintype n] (A : Matrix m n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :
    A * fromCols B₁ B₂ = fromCols (A * B₁) (A * B₂)

Proof state:
R : Type u_1
m : Type u_2
n : Type u_5
n₁ : Type u_6
n₂ : Type u_7
inst✝¹ : Semiring R
inst✝ : Fintype n
A : Matrix m n R
B₁ : Matrix n n₁ R
B₂ : Matrix n n₂ R
⊢ A * B₁.fromCols B₂ = (A * B₁).fromCols (A * B₂)

Tactic:
ext _ (_ | _) <;> simp [mul_apply]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem vanishingIdeal_singleton (x : ProjectiveSpectrum 𝒜) :
    vanishingIdeal ({x} : Set (ProjectiveSpectrum 𝒜)) = x.asHomogeneousIdeal

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
x : ProjectiveSpectrum 𝒜
⊢ vanishingIdeal {x} = x.asHomogeneousIdeal

Tactic:
simp [vanishingIdeal]

Result:
no goals
-- Mathlib/Data/Matrix/DMatrix.lean
theorem ext_iff : (∀ i j, M i j = N i j) ↔ M = N :=
  ⟨fun h => funext fun i => funext <| h i, fun h => by simp [h]⟩

Proof state:
m : Type u_1
n : Type u_2
α : m → n → Type v
M N : DMatrix m n α
h : M = N
⊢ ∀ (i : m) (j : n), M i j = N i j

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Algebra/Homology/Single.lean
@[simp]
lemma fromSingle₀Equiv_symm_apply_f_zero
    {C : ChainComplex V ℕ} {X : V} (f : X ⟶ C.X 0) :
    ((fromSingle₀Equiv C X).symm f).f 0 = f

Proof state:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
f : X ⟶ C.X 0
⊢ ((C.fromSingle₀Equiv X).symm f).f 0 = f

Tactic:
simp [fromSingle₀Equiv]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Fubini.lean
theorem colimitUncurryIsoColimitCompColim_ι_hom {j} {k} :
    colimit.ι _ (j, k) ≫ (colimitUncurryIsoColimitCompColim F).hom =
      (colimit.ι _ k ≫ colimit.ι (F ⋙ colim) j : _ ⟶ (colimit (F ⋙ colim)))

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_5, u_1} J
inst✝⁴ : Category.{u_6, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimit (uncurry.obj F)
inst✝ : HasColimit (F ⋙ colim)
j : J
k : K
⊢ colimit.ι (uncurry.obj F) (j, k) ≫ (colimitUncurryIsoColimitCompColim F).hom =
    colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j

Tactic:
rw [← cancel_mono (colimitUncurryIsoColimitCompColim F).inv]

Result:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_5, u_1} J
inst✝⁴ : Category.{u_6, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimit (uncurry.obj F)
inst✝ : HasColimit (F ⋙ colim)
j : J
k : K
⊢ (colimit.ι (uncurry.obj F) (j, k) ≫ (colimitUncurryIsoColimitCompColim F).hom) ≫
      (colimitUncurryIsoColimitCompColim F).inv =
    (colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j) ≫ (colimitUncurryIsoColimitCompColim F).inv

Proof state:
J : Type u_1
K : Type u_2
inst✝⁵ : Category.{u_5, u_1} J
inst✝⁴ : Category.{u_6, u_2} K
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
F : J ⥤ K ⥤ C
inst✝² : HasColimitsOfShape K C
inst✝¹ : HasColimit (uncurry.obj F)
inst✝ : HasColimit (F ⋙ colim)
j : J
k : K
⊢ (colimit.ι (uncurry.obj F) (j, k) ≫ (colimitUncurryIsoColimitCompColim F).hom) ≫
      (colimitUncurryIsoColimitCompColim F).inv =
    (colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j) ≫ (colimitUncurryIsoColimitCompColim F).inv

Tactic:
simp

Result:
no goals
-- Mathlib/Data/DFinsupp/Module.lean
theorem filter_smul [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)] (p : ι → Prop)
    [DecidablePred p] (r : γ) (f : Π₀ i, β i) : (r • f).filter p = r • f.filter p

Proof state:
case h
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : Monoid γ
inst✝² : (i : ι) → AddMonoid (β i)
inst✝¹ : (i : ι) → DistribMulAction γ (β i)
p : ι → Prop
inst✝ : DecidablePred p
r : γ
f : Π₀ (i : ι), β i
i✝ : ι
⊢ (filter p (r • f)) i✝ = (r • filter p f) i✝

Tactic:
simp [smul_apply, smul_ite]

Result:
no goals

Proof state:
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : Monoid γ
inst✝² : (i : ι) → AddMonoid (β i)
inst✝¹ : (i : ι) → DistribMulAction γ (β i)
p : ι → Prop
inst✝ : DecidablePred p
r : γ
f : Π₀ (i : ι), β i
⊢ filter p (r • f) = r • filter p f

Tactic:
ext

Result:
case h
ι : Type u
γ : Type w
β : ι → Type v
inst✝³ : Monoid γ
inst✝² : (i : ι) → AddMonoid (β i)
inst✝¹ : (i : ι) → DistribMulAction γ (β i)
p : ι → Prop
inst✝ : DecidablePred p
r : γ
f : Π₀ (i : ι), β i
i✝ : ι
⊢ (filter p (r • f)) i✝ = (r • filter p f) i✝
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_inv_eq (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : z ≠ 0) : x ^ z⁻¹ = y ↔ x = y ^ z

Proof state:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ x ^ z⁻¹ = y ↔ x = y ^ z

Tactic:
rw [← rpow_left_inj _ hy hz, rpow_inv_rpow hx hz]

Result:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ 0 ≤ x ^ z⁻¹

Proof state:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hz : z ≠ 0
⊢ 0 ≤ x ^ z⁻¹

Tactic:
positivity

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem angle_eq_iff_two_pi_dvd_sub {ψ θ : ℝ} : (θ : Angle) = ψ ↔ ∃ k : ℤ, θ - ψ = 2 * π * k

Proof state:
ψ θ : ℝ
⊢ ↑θ = ↑ψ ↔ ∃ k, θ - ψ = 2 * π * ↑k

Tactic:
simp only [QuotientAddGroup.eq, AddSubgroup.zmultiples_eq_closure,
  AddSubgroup.mem_closure_singleton, zsmul_eq_mul', (sub_eq_neg_add _ _).symm, eq_comm]

Result:
ψ θ : ℝ
⊢ ↑ψ = ↑θ ↔ ∃ k, θ - ψ = 2 * π * ↑k

Proof state:
ψ θ : ℝ
⊢ -ψ + θ ∈ AddSubgroup.zmultiples (2 * π) ↔ ∃ k, θ - ψ = 2 * π * ↑k

Tactic:
simp only [AddSubgroup.zmultiples_eq_closure,
  AddSubgroup.mem_closure_singleton, zsmul_eq_mul', (sub_eq_neg_add _ _).symm, eq_comm]

Result:
no goals

Proof state:
ψ θ : ℝ
⊢ ↑ψ = ↑θ ↔ ∃ k, θ - ψ = 2 * π * ↑k

Tactic:
rw [Angle.coe, Angle.coe, QuotientAddGroup.eq]

Result:
ψ θ : ℝ
⊢ -ψ + θ ∈ AddSubgroup.zmultiples (2 * π) ↔ ∃ k, θ - ψ = 2 * π * ↑k