harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma baseChange_Ψ (n : ℤ) : (W.baseChange B).Ψ n = ((W.baseChange A).Ψ n).map (mapRingHom f)

Proof state:
R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ (W.baseChange B).Ψ n = Polynomial.map (mapRingHom ↑f) ((W.baseChange A).Ψ n)

Tactic:
rw [← map_Ψ, map_baseChange]

Result:
no goals
-- Mathlib/FieldTheory/Separable.lean
theorem Separable.squarefree {p : R[X]} (hsep : Separable p) : Squarefree p

Proof state:
R : Type u
inst✝ : CommSemiring R
p : R[X]
hsep : p.Separable
⊢ ∀ (x : R[X]), emultiplicity x p ≤ 1 ∨ IsUnit x

Tactic:
exact fun f => or_iff_not_imp_right.mpr fun hunit => emultiplicity_le_one_of_separable hunit hsep

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p : R[X]
hsep : p.Separable
⊢ Squarefree p

Tactic:
rw [squarefree_iff_emultiplicity_le_one p]

Result:
R : Type u
inst✝ : CommSemiring R
p : R[X]
hsep : p.Separable
⊢ ∀ (x : R[X]), emultiplicity x p ≤ 1 ∨ IsUnit x

Proof state:
R : Type u
inst✝ : CommSemiring R
p : R[X]
hsep : p.Separable
⊢ Squarefree p

Tactic:
classical
rw [squarefree_iff_emultiplicity_le_one p]
exact fun f => or_iff_not_imp_right.mpr fun hunit => emultiplicity_le_one_of_separable hunit hsep

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
/-- This can be used for rewriting if the LHS is inside a binder and it is unknown
whether `f = e`. -/
lemma Indep.insert_diff_indep_iff (hI : M.Indep (I \ {e})) (heI : e ∈ I) :
    M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I

Proof state:
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
⊢ M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I

Tactic:
obtain rfl | hne := eq_or_ne e f

Result:
case inl
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
⊢ M.Indep (insert e I \ {e}) ↔ e ∈ M.E \ M.closure (I \ {e}) ∨ e ∈ I

case inr
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
hne : e ≠ f
⊢ M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I

Proof state:
case inr
α : Type u_2
M : Matroid α
e f : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
hne : e ≠ f
⊢ M.Indep (insert f I \ {e}) ↔ f ∈ M.E \ M.closure (I \ {e}) ∨ f ∈ I

Tactic:
rw [← insert_diff_singleton_comm hne.symm, hI.insert_indep_iff, mem_diff_singleton,
  and_iff_left hne.symm]

Result:
no goals

Proof state:
case inl
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep (I \ {e})
heI : e ∈ I
⊢ M.Indep (insert e I \ {e}) ↔ e ∈ M.E \ M.closure (I \ {e}) ∨ e ∈ I

Tactic:
simp [hI, heI]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
@[simp] lemma basisOf_smul (a : G) (b : AffineBasis ι k V) (i : ι) :
    (a • b).basisOf i = a • b.basisOf i

Proof state:
case a
ι : Type u_1
G : Type u_3
k : Type u_5
V : Type u_6
inst✝⁵ : AddCommGroup V
inst✝⁴ : Ring k
inst✝³ : Module k V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G k V
a : G
b : AffineBasis ι k V
i : ι
j : { j // j ≠ i }
⊢ ((a • b).basisOf i) j = (a • b.basisOf i) j

Tactic:
simp [smul_sub]

Result:
no goals

Proof state:
ι : Type u_1
G : Type u_3
k : Type u_5
V : Type u_6
inst✝⁵ : AddCommGroup V
inst✝⁴ : Ring k
inst✝³ : Module k V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G k V
a : G
b : AffineBasis ι k V
i : ι
⊢ (a • b).basisOf i = a • b.basisOf i

Tactic:
ext j

Result:
case a
ι : Type u_1
G : Type u_3
k : Type u_5
V : Type u_6
inst✝⁵ : AddCommGroup V
inst✝⁴ : Ring k
inst✝³ : Module k V
inst✝² : Group G
inst✝¹ : DistribMulAction G V
inst✝ : SMulCommClass G k V
a : G
b : AffineBasis ι k V
i : ι
j : { j // j ≠ i }
⊢ ((a • b).basisOf i) j = (a • b.basisOf i) j
-- Mathlib/Analysis/Fourier/ZMod.lean
lemma dft_apply_zero (Φ : ZMod N → E) : 𝓕 Φ 0 = ∑ j, Φ j

Proof state:
N : ℕ
inst✝² : NeZero N
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℂ E
Φ : ZMod N → E
⊢ 𝓕 Φ 0 = ∑ j : ZMod N, Φ j

Tactic:
simp only [dft_apply, mul_zero, neg_zero, map_zero_eq_one, one_smul]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
lemma Gammaℝ_ne_zero_of_re_pos {s : ℂ} (hs : 0 < re s) : Gammaℝ s ≠ 0

Proof state:
s : ℂ
hs : 0 < s.re
⊢ s.Gammaℝ ≠ 0

Tactic:
apply mul_ne_zero

Result:
case ha
s : ℂ
hs : 0 < s.re
⊢ ↑π ^ (-s / 2) ≠ 0

case hb
s : ℂ
hs : 0 < s.re
⊢ Gamma (s / 2) ≠ 0

Proof state:
case hb.hs
s : ℂ
hs : 0 < s.re
⊢ 0 < s.re / 2

Tactic:
exact div_pos hs two_pos

Result:
no goals

Proof state:
case ha
s : ℂ
hs : 0 < s.re
⊢ ↑π ^ (-s / 2) ≠ 0

Tactic:
simp [pi_ne_zero]

Result:
no goals

Proof state:
case hb.hs
s : ℂ
hs : 0 < s.re
⊢ 0 < (s / 2).re

Tactic:
rw [div_ofNat_re]

Result:
case hb.hs
s : ℂ
hs : 0 < s.re
⊢ 0 < s.re / 2

Proof state:
case hb
s : ℂ
hs : 0 < s.re
⊢ Gamma (s / 2) ≠ 0

Tactic:
apply Gamma_ne_zero_of_re_pos

Result:
case hb.hs
s : ℂ
hs : 0 < s.re
⊢ 0 < (s / 2).re
-- Mathlib/Probability/Kernel/WithDensity.lean
theorem lintegral_withDensity (κ : Kernel α β) [IsSFiniteKernel κ]
    (hf : Measurable (Function.uncurry f)) (a : α) {g : β → ℝ≥0∞} (hg : Measurable g) :
    ∫⁻ b, g b ∂withDensity κ f a = ∫⁻ b, f a b * g b ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
g : β → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (a_1 : β), (f a * g) a_1 ∂κ a = ∫⁻ (b : β), f a b * g b ∂κ a

Tactic:
simp_rw [Pi.mul_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
g : β → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (b : β), g b ∂(κ.withDensity f) a = ∫⁻ (b : β), f a b * g b ∂κ a

Tactic:
rw [Kernel.withDensity_apply _ hf,
  lintegral_withDensity_eq_lintegral_mul _ (Measurable.of_uncurry_left hf) hg]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
g : β → ℝ≥0∞
hg : Measurable g
⊢ ∫⁻ (a_1 : β), (f a * g) a_1 ∂κ a = ∫⁻ (b : β), f a b * g b ∂κ a
-- Mathlib/Data/ZMod/Basic.lean
lemma val_one'' : ∀ {n}, n ≠ 1 → (1 : ZMod n).val = 1
  | 0, _ => rfl
  | 1, hn => by cases hn rfl
  | n + 2, _ =>
    haveI : Fact (1 < n + 2) := ⟨by simp⟩
    ZMod.val_one _

Proof state:
n : ℕ
x✝ : n + 2 ≠ 1
⊢ 1 < n + 2

Tactic:
simp

Result:
no goals

Proof state:
hn : 1 ≠ 1
⊢ val 1 = 1

Tactic:
cases hn rfl

Result:
no goals
-- Mathlib/Algebra/Group/EvenFunction.lean
lemma Odd.add [SubtractionCommMonoid β] {f g : α → β} (hf : f.Odd) (hg : g.Odd) : (f + g).Odd

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
inst✝ : SubtractionCommMonoid β
f g : α → β
hf : Function.Odd f
hg : Function.Odd g
⊢ Function.Odd (f + g)

Tactic:
intro a

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
inst✝ : SubtractionCommMonoid β
f g : α → β
hf : Function.Odd f
hg : Function.Odd g
a : α
⊢ (f + g) (-a) = -(f + g) a

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Neg α
inst✝ : SubtractionCommMonoid β
f g : α → β
hf : Function.Odd f
hg : Function.Odd g
a : α
⊢ (f + g) (-a) = -(f + g) a

Tactic:
simp only [hf a, hg a, Pi.add_apply, neg_add]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem det_mul_add_one_comm (A : Matrix m n α) (B : Matrix n m α) :
    det (A * B + 1) = det (B * A + 1)

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m n α
B : Matrix n m α
⊢ (A * B + 1).det = (B * A + 1).det

Tactic:
rw [add_comm, det_one_add_mul_comm, add_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftedHom.lean
@[simp]
lemma mk₀_comp_mk₀ (f : X ⟶ Y) (g : Y ⟶ Z) {a b c : M} (h : b + a = c)
    (ha : a = 0) (hb : b = 0) :
    (mk₀ a ha f).comp (mk₀ b hb g) h = mk₀ c (by rw [← h, ha, hb, add_zero]) (f ≫ g)

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : 0 + 0 = 0
⊢ (mk₀ 0 ⋯ f).comp (mk₀ 0 ⋯ g) h = mk₀ 0 ⋯ (f ≫ g)

Tactic:
rw [mk₀_comp, mk₀, mk₀, assoc]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
c : M
h : 0 + 0 = c
⊢ (mk₀ 0 ⋯ f).comp (mk₀ 0 ⋯ g) h = mk₀ c ⋯ (f ≫ g)

Tactic:
obtain rfl : c = 0 := by rw [← h, zero_add]

Result:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : 0 + 0 = 0
⊢ (mk₀ 0 ⋯ f).comp (mk₀ 0 ⋯ g) h = mk₀ 0 ⋯ (f ≫ g)

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
a b c : M
h : b + a = c
ha : a = 0
hb : b = 0
⊢ (mk₀ a ha f).comp (mk₀ b hb g) h = mk₀ c ⋯ (f ≫ g)

Tactic:
subst ha hb

Result:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
c : M
h : 0 + 0 = c
⊢ (mk₀ 0 ⋯ f).comp (mk₀ 0 ⋯ g) h = mk₀ c ⋯ (f ≫ g)

Proof state:
C : Type u_1
inst✝⁶ : Category.{?u.25674, u_1} C
D : Type u_2
inst✝⁵ : Category.{?u.25681, u_2} D
E : Type u_3
inst✝⁴ : Category.{?u.25688, u_3} E
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
inst✝ : HasShift E M
X Y Z T : C
f : X ⟶ Y
g : Y ⟶ Z
a b c : M
h : b + a = c
ha : a = 0
hb : b = 0
⊢ c = 0

Tactic:
rw [← h, ha, hb, add_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
c : M
h : 0 + 0 = c
⊢ c = 0

Tactic:
rw [← h, zero_add]

Result:
no goals
-- Mathlib/Data/List/OfFn.lean
theorem ofFn_getElem : ∀ l : List α, (ofFn (fun i : Fin l.length => l[(i : Nat)])) = l
  | [] => by rw [ofFn_zero]
  | a :: l => by
    rw [ofFn_succ]
    congr
    exact ofFn_get l

Proof state:
α : Type u
a : α
l : List α
⊢ (ofFn fun i => (a :: l)[↑i]) = a :: l

Tactic:
rw [ofFn_succ]

Result:
α : Type u
a : α
l : List α
⊢ ((a :: l)[↑0] :: ofFn fun i => (a :: l)[↑i.succ]) = a :: l

Proof state:
α : Type u
⊢ (ofFn fun i => [][↑i]) = []

Tactic:
rw [ofFn_zero]

Result:
no goals

Proof state:
case e_tail
α : Type u
a : α
l : List α
⊢ (ofFn fun i => (a :: l)[↑i.succ]) = l

Tactic:
exact ofFn_get l

Result:
no goals

Proof state:
α : Type u
a : α
l : List α
⊢ ((a :: l)[↑0] :: ofFn fun i => (a :: l)[↑i.succ]) = a :: l

Tactic:
congr

Result:
case e_tail
α : Type u
a : α
l : List α
⊢ (ofFn fun i => (a :: l)[↑i.succ]) = l
-- Mathlib/RingTheory/SimpleRing/Basic.lean
lemma iff_injective_ringHom (R : Type u) [NonAssocRing R] [Nontrivial R] :
    IsSimpleRing R ↔
    ∀ {S : Type u} [NonAssocSemiring S] [Nontrivial S] (f : R →+* S), Function.Injective f :=
  iff_injective_ringHom_or_subsingleton_codomain R |>.trans <|
    ⟨fun H _ _ _ f => H f |>.resolve_right (by simpa [not_subsingleton_iff_nontrivial]),
      fun H S _ f => subsingleton_or_nontrivial S |>.recOn Or.inr fun _ => Or.inl <| H f⟩

Proof state:
R : Type u
inst✝¹ : NonAssocRing R
inst✝ : Nontrivial R
H : ∀ {S : Type u} [inst : NonAssocSemiring S] (f : R →+* S), Function.Injective ⇑f ∨ Subsingleton S
x✝² : Type u
x✝¹ : NonAssocSemiring x✝²
x✝ : Nontrivial x✝²
f : R →+* x✝²
⊢ ¬Subsingleton x✝²

Tactic:
simpa [not_subsingleton_iff_nontrivial]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mul_le_add_right {m k n : Nat} : k * m ≤ m + n ↔ (k-1) * m ≤ n

Proof state:
m k n : Nat
⊢ k * m ≤ m + n ↔ (k - 1) * m ≤ n

Tactic:
match k with
| 0 =>
  simp
| succ k =>
  simp [succ_mul, Nat.add_comm _ m, Nat.add_le_add_iff_left]

Result:
no goals

Proof state:
m k✝ n k : Nat
⊢ k.succ * m ≤ m + n ↔ (k.succ - 1) * m ≤ n

Tactic:
simp [succ_mul, Nat.add_comm _ m, Nat.add_le_add_iff_left]

Result:
no goals

Proof state:
m k n : Nat
⊢ 0 * m ≤ m + n ↔ (0 - 1) * m ≤ n

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/FunctorCategory/Basic.lean
theorem colimitObjIsoColimitCompEvaluation_inv_colimit_map [HasColimitsOfShape J C] (F : J ⥤ K ⥤ C)
    {i j : K} (f : i ⟶ j) :
    (colimitObjIsoColimitCompEvaluation _ _).inv ≫ (colimit F).map f =
      colimMap (whiskerLeft _ ((evaluation _ _).map f)) ≫
        (colimitObjIsoColimitCompEvaluation _ _).inv

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
i j : K
f : i ⟶ j
⊢ (colimitObjIsoColimitCompEvaluation F i).inv ≫ (colimit F).map f =
    colimMap (whiskerLeft F ((evaluation K C).map f)) ≫ (colimitObjIsoColimitCompEvaluation F j).inv

Tactic:
ext

Result:
case w
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
i j : K
f : i ⟶ j
j✝ : J
⊢ colimit.ι (F ⋙ (evaluation K C).obj i) j✝ ≫ (colimitObjIsoColimitCompEvaluation F i).inv ≫ (colimit F).map f =
    colimit.ι (F ⋙ (evaluation K C).obj i) j✝ ≫
      colimMap (whiskerLeft F ((evaluation K C).map f)) ≫ (colimitObjIsoColimitCompEvaluation F j).inv

Proof state:
case w
C : Type u
inst✝³ : Category.{v, u} C
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
inst✝ : HasColimitsOfShape J C
F : J ⥤ K ⥤ C
i j : K
f : i ⟶ j
j✝ : J
⊢ colimit.ι (F ⋙ (evaluation K C).obj i) j✝ ≫ (colimitObjIsoColimitCompEvaluation F i).inv ≫ (colimit F).map f =
    colimit.ι (F ⋙ (evaluation K C).obj i) j✝ ≫
      colimMap (whiskerLeft F ((evaluation K C).map f)) ≫ (colimitObjIsoColimitCompEvaluation F j).inv

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma add_eq_three_iff :
    m + n = 3 ↔ m = 0 ∧ n = 3 ∨ m = 1 ∧ n = 2 ∨ m = 2 ∧ n = 1 ∨ m = 3 ∧ n = 0

Proof state:
m n : ℕ
⊢ m + n = 3 ↔ m = 0 ∧ n = 3 ∨ m = 1 ∧ n = 2 ∨ m = 2 ∧ n = 1 ∨ m = 3 ∧ n = 0

Tactic:
omega

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem linearCombination_smul [Module R S] [Module S M] [IsScalarTower R S M] {w : α' → S} :
    linearCombination R (fun i : α × α' ↦ w i.2 • v i.1) = (linearCombination S v).restrictScalars R
      ∘ₗ mapRange.linearMap (linearCombination R w) ∘ₗ (finsuppProdLEquiv R).toLinearMap

Proof state:
case h.h
α : Type u_1
M : Type u_2
R : Type u_5
S : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
α' : Type u_7
v : α → M
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
w : α' → S
a✝ : α × α'
⊢ ((linearCombination R fun i => w i.2 • v i.1) ∘ₗ lsingle a✝) 1 =
    ((↑R (linearCombination S v) ∘ₗ mapRange.linearMap (linearCombination R w) ∘ₗ ↑(finsuppProdLEquiv R)) ∘ₗ lsingle a✝)
      1

Tactic:
simp [finsuppProdLEquiv, finsuppProdEquiv, Finsupp.curry]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
S : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
α' : Type u_7
v : α → M
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
w : α' → S
⊢ (linearCombination R fun i => w i.2 • v i.1) =
    ↑R (linearCombination S v) ∘ₗ mapRange.linearMap (linearCombination R w) ∘ₗ ↑(finsuppProdLEquiv R)

Tactic:
ext

Result:
case h.h
α : Type u_1
M : Type u_2
R : Type u_5
S : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
α' : Type u_7
v : α → M
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
w : α' → S
a✝ : α × α'
⊢ ((linearCombination R fun i => w i.2 • v i.1) ∘ₗ lsingle a✝) 1 =
    ((↑R (linearCombination S v) ∘ₗ mapRange.linearMap (linearCombination R w) ∘ₗ ↑(finsuppProdLEquiv R)) ∘ₗ lsingle a✝)
      1
-- Mathlib/Order/SuccPred/Basic.lean
theorem Icc_subset_Ioc_pred_left_of_not_isMin (ha : ¬IsMin a) : Icc a b ⊆ Ioc (pred a) b

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ Icc a b ⊆ Ioc (pred a) b

Tactic:
rw [← Ioi_inter_Iic, ← Ici_inter_Iic]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ Ici a ∩ Iic b ⊆ Ioi (pred a) ∩ Iic b

Proof state:
case H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ Ici a ⊆ Ioi (pred a)

Tactic:
apply Ici_subset_Ioi_pred_of_not_isMin ha

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ Ici a ∩ Iic b ⊆ Ioi (pred a) ∩ Iic b

Tactic:
gcongr

Result:
case H
α : Type u_1
inst✝¹ : Preorder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
⊢ Ici a ⊆ Ioi (pred a)
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem two_le_iff' (x : α) : (2 : Cardinal) ≤ #α ↔ ∃ y : α, y ≠ x

Proof state:
α : Type u
x : α
⊢ 2 ≤ #α ↔ ∃ y, y ≠ x

Tactic:
rw [two_le_iff, ← nontrivial_iff, nontrivial_iff_exists_ne x]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma IsMeasurableRatCDF.measurable_measure_stieltjesFunction :
    Measurable fun a ↦ (hf.stieltjesFunction a).measure

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
⊢ Measurable fun a => (hf.stieltjesFunction a).measure

Tactic:
apply_rules [StieltjesFunction.measurable_measure, measurable_stieltjesFunction,
  tendsto_stieltjesFunction_atBot, tendsto_stieltjesFunction_atTop]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} (h : m.WF) :
    (Const.modify m k f).contains k' = m.contains k'

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : β → β
h : m.WF
⊢ (modify m k f).contains k' = m.contains k'

Tactic:
simp_to_raw using Raw₀.Const.contains_modify

Result:
no goals
-- Mathlib/Topology/Algebra/Valued/NormedValued.lean
theorem norm_add_le (x y : L) : norm (x + y) ≤ max (norm x) (norm y)

Proof state:
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x y : L
⊢ v (x + y) ≤ v x ∨ v (x + y) ≤ v y

Tactic:
exact le_max_iff.mp (Valuation.map_add_le_max' val.v _ _)

Result:
no goals

Proof state:
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x y : L
⊢ norm (x + y) ≤ norm x ⊔ norm y

Tactic:
simp only [norm, NNReal.coe_le_coe, le_max_iff, StrictMono.le_iff_le hv.strictMono]

Result:
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x y : L
⊢ v (x + y) ≤ v x ∨ v (x + y) ≤ v y
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem isUniformEmbedding_inl : IsUniformEmbedding (Sum.inl : α → α ⊕ β) :=
  isUniformEmbedding_iff'.2 ⟨Sum.inl_injective, uniformContinuous_inl, fun s hs =>
    ⟨Prod.map Sum.inl Sum.inl '' s ∪ range (Prod.map Sum.inr Sum.inr),
      union_mem_sup (image_mem_map hs) range_mem_map,
      fun x h => by simpa [Prod.map_apply'] using h⟩⟩

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (α × α)
hs : s ∈ 𝓤 α
x : α × α
h : x ∈ Prod.map Sum.inl Sum.inl ⁻¹' (Prod.map Sum.inl Sum.inl '' s ∪ range (Prod.map Sum.inr Sum.inr))
⊢ x ∈ s

Tactic:
simpa [Prod.map_apply'] using h

Result:
no goals
-- Mathlib/AlgebraicGeometry/Stalk.lean
@[reassoc (attr := simp)]
lemma Spec_map_stalkSpecializes_fromSpecStalk {x y : X} (h : x ⤳ y) :
    Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x

Proof state:
case intro.intro.intro.intro.intro
X : Scheme
x y : ↑↑X.toPresheafedSpace
h : x ⤳ y
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hyU : y ∈ ↑U
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x

Tactic:
have hxU : x ∈ U := h.mem_open U.2 hyU

Result:
case intro.intro.intro.intro.intro
X : Scheme
x y : ↑↑X.toPresheafedSpace
h : x ⤳ y
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hyU : y ∈ ↑U
hxU : x ∈ U
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x

Proof state:
case intro.intro.intro.intro.intro
X : Scheme
x y : ↑↑X.toPresheafedSpace
h : x ⤳ y
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hyU : y ∈ ↑U
hxU : x ∈ U
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x

Tactic:
rw [← hU.fromSpecStalk_eq_fromSpecStalk hyU, ← hU.fromSpecStalk_eq_fromSpecStalk hxU,
  IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpecStalk, ← Category.assoc, ← Spec.map_comp,
  TopCat.Presheaf.germ_stalkSpecializes]

Result:
no goals

Proof state:
X : Scheme
x y : ↑↑X.toPresheafedSpace
h : x ⤳ y
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hyU, -⟩ :=
  (isBasis_affine_open X).exists_subset_of_mem_open (Set.mem_univ y) isOpen_univ

Result:
case intro.intro.intro.intro.intro
X : Scheme
x y : ↑↑X.toPresheafedSpace
h : x ⤳ y
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hyU : y ∈ ↑U
⊢ Spec.map (X.presheaf.stalkSpecializes h) ≫ X.fromSpecStalk y = X.fromSpecStalk x
-- Mathlib/MeasureTheory/Measure/Tight.lean
/-- In a compact space, every set of measures is tight. -/
lemma of_compactSpace [CompactSpace α] : IsTightMeasureSet S

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
mα : MeasurableSpace α
S : Set (Measure α)
inst✝ : CompactSpace α
⊢ IsTightMeasureSet S

Tactic:
simp only [IsTightMeasureSet, cocompact_eq_bot, smallSets_bot, tendsto_pure_left, iSup_apply,
  measure_empty, ENNReal.iSup_zero, ciSup_const]

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
mα : MeasurableSpace α
S : Set (Measure α)
inst✝ : CompactSpace α
⊢ ∀ s ∈ 𝓝 0, 0 ∈ s

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
mα : MeasurableSpace α
S : Set (Measure α)
inst✝ : CompactSpace α
⊢ ∀ s ∈ 𝓝 0, 0 ∈ s

Tactic:
exact fun _ ↦ mem_of_mem_nhds

Result:
no goals
-- Mathlib/Data/Finset/Sigma.lean
theorem _root_.biSup_finsetSigma [CompleteLattice β] (s : Finset ι) (t : ∀ i, Finset (α i))
    (f : Sigma α → β) : ⨆ ij ∈ s.sigma t, f ij = ⨆ (i ∈ s) (j ∈ t i), f ⟨i, j⟩

Proof state:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst✝ : CompleteLattice β
s : Finset ι
t : (i : ι) → Finset (α i)
f : Sigma α → β
⊢ ⨆ ij ∈ s.sigma t, f ij = ⨆ i ∈ s, ⨆ j ∈ t i, f ⟨i, j⟩

Tactic:
simp_rw [← Finset.iSup_coe, Finset.coe_sigma, biSup_sigma]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Cooper.lean
theorem dvd_of_mul_dvd {a b c : Int} (w : a * b ∣ a * c) (h : 0 < a) : b ∣ c

Proof state:
a b c : Int
w : a * b ∣ a * c
h : 0 < a
⊢ b ∣ c

Tactic:
obtain ⟨z, w⟩ := w

Result:
case intro
a b c : Int
h : 0 < a
z : Int
w : a * c = a * b * z
⊢ b ∣ c

Proof state:
case intro
a b c : Int
h : 0 < a
z : Int
w : a * c = a * b * z
⊢ b ∣ c

Tactic:
refine ⟨z, ?_⟩

Result:
case intro
a b c : Int
h : 0 < a
z : Int
w : a * c = a * b * z
⊢ c = b * z

Proof state:
case intro
a b c : Int
h : 0 < a
z : Int
w : (fun x => x / a) (a * c) = (fun x => x / a) (a * b * z)
⊢ c = b * z

Tactic:
dsimp at w

Result:
case intro
a b c : Int
h : 0 < a
z : Int
w : a * c / a = a * b * z / a
⊢ c = b * z

Proof state:
case intro
a b c : Int
h : 0 < a
z : Int
w : a * c / a = a * b * z / a
⊢ c = b * z

Tactic:
rwa [Int.mul_ediv_cancel_left _ (Int.ne_of_gt h), Int.mul_assoc,
  Int.mul_ediv_cancel_left _ (Int.ne_of_gt h)] at w

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
theorem mem_disjSups : c ∈ s ○ t ↔ ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t : Finset α
c : α
⊢ c ∈ s ○ t ↔ ∃ a ∈ s, ∃ b ∈ t, Disjoint a b ∧ a ⊔ b = c

Tactic:
simp [disjSups, and_assoc]

Result:
no goals