harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
@[simp] lemma ofIsColimitCokernelCofork_g' (hg : S.g = 0) (c : CokernelCofork S.f)
  (hc : IsColimit c) : (ofIsColimitCokernelCofork S hg c hc).g' = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ (ofIsColimitCokernelCofork S hg c hc).g' = 0

Tactic:
rw [← cancel_epi (ofIsColimitCokernelCofork S hg c hc).p, p_g', hg, comp_zero]

Result:
no goals
-- Mathlib/Order/Iterate.lean
theorem iterate_pos_lt_of_map_lt (h : Commute f g) (hf : Monotone f) (hg : StrictMono g) {x}
    (hx : f x < g x) {n} (hn : 0 < n) : f^[n] x < g^[n] x

Proof state:
case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
k✝ : ℕ
a✝ : k✝ < n
⊢ f^[k✝ + 1] x ≤ f (f^[k✝] x)

Tactic:
rw [iterate_succ_apply']

Result:
no goals

Proof state:
case h₀
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ f^[0] x ≤ g^[0] x

Tactic:
rfl

Result:
no goals

Proof state:
case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) < g^[k + 1] x

Tactic:
intros

Result:
case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
k✝ : ℕ
a✝ : k✝ < n
⊢ f (g^[k✝] x) < g^[k✝ + 1] x

Proof state:
case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)

Tactic:
intros

Result:
case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
k✝ : ℕ
a✝ : k✝ < n
⊢ f^[k✝ + 1] x ≤ f (f^[k✝] x)

Proof state:
case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
k✝ : ℕ
a✝ : k✝ < n
⊢ f (g^[k✝] x) < g^[k✝ + 1] x

Tactic:
simp [h.iterate_right _ _, hg.iterate _ hx]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ f^[n] x < g^[n] x

Tactic:
apply hf.seq_pos_lt_seq_of_le_of_lt hn

Result:
case h₀
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ f^[0] x ≤ g^[0] x

case hx
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)

case hy
α : Type u_1
inst✝ : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ ∀ (k : ℕ), k < n → f (g^[k] x) < g^[k + 1] x
-- Mathlib/Data/Multiset/Sum.lean
theorem Nodup.disjSum (hs : s.Nodup) (ht : t.Nodup) : (s.disjSum t).Nodup

Proof state:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
⊢ (s.disjSum t).Nodup

Tactic:
refine ((hs.map inl_injective).add_iff <| ht.map inr_injective).2 ?_

Result:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
⊢ Disjoint (Multiset.map inl s) (Multiset.map inr t)

Proof state:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
⊢ Disjoint (Multiset.map inl s) (Multiset.map inr t)

Tactic:
rw [disjoint_map_map]

Result:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
⊢ ∀ a ∈ s, ∀ b ∈ t, inl a ≠ inr b

Proof state:
α : Type u_1
β : Type u_2
s : Multiset α
t : Multiset β
hs : s.Nodup
ht : t.Nodup
⊢ ∀ a ∈ s, ∀ b ∈ t, inl a ≠ inr b

Tactic:
exact fun _ _ _ _ ↦ inr_ne_inl.symm

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Finset.lean
lemma tendsto_toLeft_atTop :
    Tendsto (Finset.toLeft (α := α) (β := β)) atTop atTop

Proof state:
α : Type u_3
β : Type u_4
⊢ Tendsto Finset.toLeft atTop atTop

Tactic:
intro s hs

Result:
α : Type u_3
β : Type u_4
s : Set (Finset α)
hs : s ∈ atTop
⊢ s ∈ map Finset.toLeft atTop

Proof state:
α : Type u_3
β : Type u_4
s : Set (Finset α)
hs : ∃ a, ∀ b ≥ a, b ∈ s
⊢ ∃ a, ∀ b ≥ a, b.toLeft ∈ s

Tactic:
obtain ⟨t, H⟩ := hs

Result:
case intro
α : Type u_3
β : Type u_4
s : Set (Finset α)
t : Finset α
H : ∀ b ≥ t, b ∈ s
⊢ ∃ a, ∀ b ≥ a, b.toLeft ∈ s

Proof state:
α : Type u_3
β : Type u_4
s : Set (Finset α)
hs : s ∈ atTop
⊢ s ∈ map Finset.toLeft atTop

Tactic:
simp only [mem_atTop_sets, Finset.le_eq_subset, Filter.mem_map, Set.mem_preimage] at hs ⊢

Result:
α : Type u_3
β : Type u_4
s : Set (Finset α)
hs : ∃ a, ∀ b ≥ a, b ∈ s
⊢ ∃ a, ∀ b ≥ a, b.toLeft ∈ s

Proof state:
α : Type u_3
β : Type u_4
s : Set (Finset α)
t : Finset α
H : ∀ b ≥ t, b ∈ s
b : Finset (α ⊕ β)
hb : b ≥ t.disjSum ∅
⊢ b.toLeft ≥ t

Tactic:
simpa [← Finset.coe_subset, Set.subset_def] using hb

Result:
no goals

Proof state:
case intro
α : Type u_3
β : Type u_4
s : Set (Finset α)
t : Finset α
H : ∀ b ≥ t, b ∈ s
⊢ ∃ a, ∀ b ≥ a, b.toLeft ∈ s

Tactic:
exact ⟨t.disjSum ∅, fun b hb ↦ H _ (by simpa [← Finset.coe_subset, Set.subset_def] using hb)⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SizeOfLemmas.lean
theorem BitVec.sizeOf (a : BitVec w) : sizeOf a = sizeOf a.toFin + 1

Proof state:
case ofFin
w : Nat
toFin✝ : Fin (2 ^ w)
⊢ sizeOf { toFin := toFin✝ } = sizeOf { toFin := toFin✝ }.toFin + 1

Tactic:
simp_arith

Result:
no goals

Proof state:
w : Nat
a : BitVec w
⊢ sizeOf a = sizeOf a.toFin + 1

Tactic:
cases a

Result:
case ofFin
w : Nat
toFin✝ : Fin (2 ^ w)
⊢ sizeOf { toFin := toFin✝ } = sizeOf { toFin := toFin✝ }.toFin + 1
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem mul_charP_coeff_zero [CharP R p] (x : 𝕎 R) : (x * p).coeff 0 = 0

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ (x * ↑p).coeff 0 = 0

Tactic:
rw [← frobenius_verschiebung, coeff_frobenius_charP, verschiebung_coeff_zero,
  zero_pow hp.out.ne_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem neg_pi_div_two_le_arg_iff {z : ℂ} : -(π / 2) ≤ arg z ↔ 0 ≤ re z ∨ 0 ≤ im z

Proof state:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.re ≠ 0

case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ 0 < ‖z‖

Tactic:
exacts [hre.ne, norm_pos_iff.mpr <| ne_of_apply_ne re hre.ne]

Result:
no goals

Proof state:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.im

Tactic:
simp only [him.not_le]

Result:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ -(π / 2) ≤ z.arg ↔ False

Proof state:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.im

Tactic:
simp only [him]

Result:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ z.arg ↔ True

Proof state:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ -(π / 2) ≤ z.arg ↔ False

Tactic:
rw [iff_false, not_le, arg_of_re_neg_of_im_neg hre him, sub_lt_iff_lt_add', ←
  sub_eq_add_neg, sub_half, Real.arcsin_lt_pi_div_two, div_lt_one, neg_im, ← abs_of_neg him,
  abs_im_lt_norm]

Result:
case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ z.re ≠ 0

case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ 0 < ‖z‖

Proof state:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ Real.arcsin ((-z).im / ‖z‖) + π

Tactic:
exact (Real.neg_pi_div_two_le_arcsin _).trans (le_add_of_nonneg_right Real.pi_pos.le)

Result:
no goals

Proof state:
case inr
z : ℂ
hre : z.re < 0
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.im

Tactic:
rcases le_or_lt 0 (im z) with him | him

Result:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.im

case inr.inr
z : ℂ
hre : z.re < 0
him : z.im < 0
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.im

Proof state:
z : ℂ
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im

Tactic:
rcases le_or_lt 0 (re z) with hre | hre

Result:
case inl
z : ℂ
hre : 0 ≤ z.re
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im

case inr
z : ℂ
hre : z.re < 0
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im

Proof state:
case inl
z : ℂ
hre : 0 ≤ z.re
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im

Tactic:
simp only [hre, arg_of_re_nonneg hre, Real.neg_pi_div_two_le_arcsin, true_or]

Result:
no goals

Proof state:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ z.arg ↔ True

Tactic:
rw [iff_true, arg_of_re_neg_of_im_nonneg hre him]

Result:
case inr.inl
z : ℂ
hre : z.re < 0
him : 0 ≤ z.im
⊢ -(π / 2) ≤ Real.arcsin ((-z).im / ‖z‖) + π

Proof state:
case inr
z : ℂ
hre : z.re < 0
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im

Tactic:
simp only [hre.not_le, false_or]

Result:
case inr
z : ℂ
hre : z.re < 0
⊢ -(π / 2) ≤ z.arg ↔ 0 ≤ z.im
-- Mathlib/RingTheory/Norm/Transitivity.lean
lemma eval_zero_det_det : eval 0 (f.polyToMatrix (cornerAddX M k).det).det = (f M.det).det

Proof state:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ (f ((evalRingHom 0).mapMatrix (cornerAddX M k)).det).det = (f M.det).det

Tactic:
congr

Result:
case e_M.h.e_6.h.e_M
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ (evalRingHom 0).mapMatrix (cornerAddX M k) = M

Proof state:
case e_M.h.e_6.h.e_M
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ (evalRingHom 0).mapMatrix (cornerAddX M k) = M

Tactic:
ext

Result:
case e_M.h.e_6.h.e_M.a
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
i✝ j✝ : m
⊢ (evalRingHom 0).mapMatrix (cornerAddX M k) i✝ j✝ = M i✝ j✝

Proof state:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ eval 0 (f.polyToMatrix (cornerAddX M k).det).det = (f M.det).det

Tactic:
rw [← coe_evalRingHom, RingHom.map_det, ← RingHom.comp_apply,
  evalRingHom_mapMatrix_comp_polyToMatrix, f.comp_apply, RingHom.map_det]

Result:
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
⊢ (f ((evalRingHom 0).mapMatrix (cornerAddX M k)).det).det = (f M.det).det

Proof state:
case e_M.h.e_6.h.e_M.a
R : Type u_1
S : Type u_2
n : Type u_4
m : Type u_5
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
M : Matrix m m S
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
k : m
inst✝¹ : Fintype m
inst✝ : Fintype n
f : S →+* Matrix n n R
i✝ j✝ : m
⊢ (evalRingHom 0).mapMatrix (cornerAddX M k) i✝ j✝ = M i✝ j✝

Tactic:
simp [cornerAddX, diagonal, apply_ite]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sin_sub_pi_div_two (θ : Angle) : sin (θ - ↑(π / 2)) = -cos θ

Proof state:
θ : Angle
⊢ (θ - ↑(π / 2)).sin = -θ.cos

Tactic:
induction θ using Real.Angle.induction_on

Result:
case h
x✝ : ℝ
⊢ (↑x✝ - ↑(π / 2)).sin = -(↑x✝).cos

Proof state:
case h
x✝ : ℝ
⊢ (↑x✝ - ↑(π / 2)).sin = -(↑x✝).cos

Tactic:
exact Real.sin_sub_pi_div_two _

Result:
no goals
-- Mathlib/Algebra/Order/Nonneg/Basic.lean
theorem toNonneg_lt {a : { x : α // 0 ≤ x }} {b : α} : a < toNonneg b ↔ ↑a < b

Proof state:
case mk
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
b a : α
ha : 0 ≤ a
⊢ ⟨a, ha⟩ < toNonneg b ↔ ↑⟨a, ha⟩ < b

Tactic:
simp [toNonneg, ha.not_lt]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
a : { x // 0 ≤ x }
b : α
⊢ a < toNonneg b ↔ ↑a < b

Tactic:
obtain ⟨a, ha⟩ := a

Result:
case mk
α : Type u_1
inst✝¹ : Zero α
inst✝ : LinearOrder α
b a : α
ha : 0 ≤ a
⊢ ⟨a, ha⟩ < toNonneg b ↔ ↑⟨a, ha⟩ < b
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem factorization_prod {α : Type*} {S : Finset α} {g : α → ℕ} (hS : ∀ x ∈ S, g x ≠ 0) :
    (S.prod g).factorization = S.sum fun x => (g x).factorization

Proof state:
case h.refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
p : ℕ
⊢ ∀ {a : α} {s : Finset α},
    a ∈ S →
      s ⊆ S →
        a ∉ s →
          (s.prod g).factorization p = (∑ x ∈ s, (g x).factorization) p →
            ((insert a s).prod g).factorization p = (∑ x ∈ insert a s, (g x).factorization) p

Tactic:
intro x T hxS hTS hxT IH

Result:
case h.refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
p : ℕ
x : α
T : Finset α
hxS : x ∈ S
hTS : T ⊆ S
hxT : x ∉ T
IH : (T.prod g).factorization p = (∑ x ∈ T, (g x).factorization) p
⊢ ((insert x T).prod g).factorization p = (∑ x ∈ insert x T, (g x).factorization) p

Proof state:
case h
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
p : ℕ
⊢ (S.prod g).factorization p = (∑ x ∈ S, (g x).factorization) p

Tactic:
refine Finset.induction_on' S ?_ ?_

Result:
case h.refine_1
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
p : ℕ
⊢ (∅.prod g).factorization p = (∑ x ∈ ∅, (g x).factorization) p

case h.refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
p : ℕ
⊢ ∀ {a : α} {s : Finset α},
    a ∈ S →
      s ⊆ S →
        a ∉ s →
          (s.prod g).factorization p = (∑ x ∈ s, (g x).factorization) p →
            ((insert a s).prod g).factorization p = (∑ x ∈ insert a s, (g x).factorization) p

Proof state:
case h.refine_1
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
p : ℕ
⊢ (∅.prod g).factorization p = (∑ x ∈ ∅, (g x).factorization) p

Tactic:
simp

Result:
no goals

Proof state:
case h.refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
p : ℕ
x : α
T : Finset α
hxS : x ∈ S
hTS : T ⊆ S
hxT : x ∉ T
IH : (T.prod g).factorization p = (∑ x ∈ T, (g x).factorization) p
⊢ ((insert x T).prod g).factorization p = (∑ x ∈ insert x T, (g x).factorization) p

Tactic:
have hT : T.prod g ≠ 0 := prod_ne_zero_iff.mpr fun x hx => hS x (hTS hx)

Result:
case h.refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
p : ℕ
x : α
T : Finset α
hxS : x ∈ S
hTS : T ⊆ S
hxT : x ∉ T
IH : (T.prod g).factorization p = (∑ x ∈ T, (g x).factorization) p
hT : T.prod g ≠ 0
⊢ ((insert x T).prod g).factorization p = (∑ x ∈ insert x T, (g x).factorization) p

Proof state:
case h.refine_2
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
p : ℕ
x : α
T : Finset α
hxS : x ∈ S
hTS : T ⊆ S
hxT : x ∉ T
IH : (T.prod g).factorization p = (∑ x ∈ T, (g x).factorization) p
hT : T.prod g ≠ 0
⊢ ((insert x T).prod g).factorization p = (∑ x ∈ insert x T, (g x).factorization) p

Tactic:
simp [prod_insert hxT, sum_insert hxT, IH, factorization_mul (hS x hxS) hT]

Result:
no goals

Proof state:
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
⊢ (S.prod g).factorization = ∑ x ∈ S, (g x).factorization

Tactic:
ext p

Result:
case h
α : Type u_1
S : Finset α
g : α → ℕ
hS : ∀ x ∈ S, g x ≠ 0
p : ℕ
⊢ (S.prod g).factorization p = (∑ x ∈ S, (g x).factorization) p
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_coe_nhds_top {f : α → ℝ≥0} {l : Filter α} :
    Tendsto (fun x => (f x : ℝ≥0∞)) l (𝓝 ∞) ↔ Tendsto f l atTop

Proof state:
α : Type u_1
f : α → ℝ≥0
l : Filter α
⊢ (∀ (x : ℝ≥0), ∀ᶠ (a : α) in l, ↑x < ↑(f a)) ↔ ∀ (i : ℝ≥0), True → ∀ᶠ (x : α) in l, f x ∈ Ioi i

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ≥0
l : Filter α
⊢ Tendsto (fun x => ↑(f x)) l (𝓝 ⊤) ↔ Tendsto f l atTop

Tactic:
rw [tendsto_nhds_top_iff_nnreal, atTop_basis_Ioi.tendsto_right_iff]

Result:
α : Type u_1
f : α → ℝ≥0
l : Filter α
⊢ (∀ (x : ℝ≥0), ∀ᶠ (a : α) in l, ↑x < ↑(f a)) ↔ ∀ (i : ℝ≥0), True → ∀ᶠ (x : α) in l, f x ∈ Ioi i
-- Mathlib/Algebra/Order/Sub/Unbundled/Basic.lean
theorem add_tsub_assoc_of_le (hc : AddLECancellable c) (h : c ≤ b) (a : α) :
    a + b - c = a + (b - c)

Proof state:
α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
b c : α
hc : AddLECancellable c
h : c ≤ b
a : α
⊢ a + b - c = a + (b - c)

Tactic:
conv_lhs => rw [← add_tsub_cancel_of_le h, add_comm c, ← add_assoc, hc.add_tsub_cancel_right]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Basic.lean
lemma pow_mul_term_eq (f : ℕ → ℂ) (s : ℂ) (n : ℕ) :
    (n + 1) ^ s * term f s (n + 1) = f (n + 1)

Proof state:
f : ℕ → ℂ
s : ℂ
n : ℕ
⊢ (↑n + 1) ^ s * term f s (n + 1) = f (n + 1)

Tactic:
simp [term, natCast_add_one_cpow_ne_zero n _, mul_comm (f _), mul_div_assoc']

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Types.lean
theorem eval_map (S : Type uᵒᵖ ⥤ Type u) (α β) (f : β ⟶ α) (s x) :
    eval S β (S.map f.op s) x = eval S α s (f x)

Proof state:
S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : S.obj (op α)
x : β
⊢ S.map ((↾fun x_1 => x) ≫ f).op s = S.map (↾fun x_1 => f x).op s

Tactic:
rfl

Result:
no goals

Proof state:
S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : S.obj (op α)
x : β
⊢ eval S β (S.map f.op s) x = eval S α s (f x)

Tactic:
simp_rw [eval, ← FunctorToTypes.map_comp_apply, ← op_comp]

Result:
S : Type uᵒᵖ ⥤ Type u
α β : Type u
f : β ⟶ α
s : S.obj (op α)
x : β
⊢ S.map ((↾fun x_1 => x) ≫ f).op s = S.map (↾fun x_1 => f x).op s
-- Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
theorem mem_sInf {S : Set (Subalgebra R A)} {x : A} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Proof state:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Set (Subalgebra R A)
x : A
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
simp only [← SetLike.mem_coe, coe_sInf, Set.mem_iInter₂]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem finiteDimensional_adjoin {S : Set L} [Finite S] (hS : ∀ x ∈ S, IsIntegral K x) :
    FiniteDimensional K (adjoin K S)

Proof state:
K : Type u
inst✝³ : Field K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
S : Set L
inst✝ : Finite ↑S
hS : ∀ x ∈ S, IsIntegral K x
⊢ FiniteDimensional K ↥(⨆ i, K⟮↑i⟯)

Tactic:
haveI (x : S) := adjoin.finiteDimensional (hS x.1 x.2)

Result:
K : Type u
inst✝³ : Field K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
S : Set L
inst✝ : Finite ↑S
hS : ∀ x ∈ S, IsIntegral K x
this : ∀ (x : ↑S), FiniteDimensional K ↥K⟮↑x⟯
⊢ FiniteDimensional K ↥(⨆ i, K⟮↑i⟯)

Proof state:
K : Type u
inst✝³ : Field K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
S : Set L
inst✝ : Finite ↑S
hS : ∀ x ∈ S, IsIntegral K x
this : ∀ (x : ↑S), FiniteDimensional K ↥K⟮↑x⟯
⊢ FiniteDimensional K ↥(⨆ i, K⟮↑i⟯)

Tactic:
exact finiteDimensional_iSup_of_finite

Result:
no goals

Proof state:
K : Type u
inst✝³ : Field K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
S : Set L
inst✝ : Finite ↑S
hS : ∀ x ∈ S, IsIntegral K x
⊢ FiniteDimensional K ↥(adjoin K S)

Tactic:
rw [← biSup_adjoin_simple, ← iSup_subtype'']

Result:
K : Type u
inst✝³ : Field K
L : Type u_3
inst✝² : Field L
inst✝¹ : Algebra K L
S : Set L
inst✝ : Finite ↑S
hS : ∀ x ∈ S, IsIntegral K x
⊢ FiniteDimensional K ↥(⨆ i, K⟮↑i⟯)
-- Mathlib/Logic/IsEmpty.lean
theorem rightTotal_iff_isEmpty_right [IsEmpty α] : RightTotal R ↔ IsEmpty β

Proof state:
α : Type u_4
β : Type u_5
R : α → β → Prop
inst✝ : IsEmpty α
⊢ RightTotal R ↔ IsEmpty β

Tactic:
simp only [RightTotal, IsEmpty.exists_iff, isEmpty_iff, imp_self]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
theorem subgroup_mul_singleton {H : Subgroup G} {h : G} (hh : h ∈ H) : (H : Set G) * {h} = H

Proof state:
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ ↑H * {h} = ↑H

Tactic:
simp [preimage, mul_mem_cancel_right (inv_mem hh)]

Result:
no goals
-- Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean
theorem smoothSheafCommRing.nonunits_stalk (x : M) :
    nonunits ((smoothSheafCommRing IM 𝓘(𝕜) M 𝕜).presheaf.stalk x)
    = RingHom.ker (smoothSheafCommRing.eval IM 𝓘(𝕜) M 𝕜 x)

Proof state:
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
⊢ nonunits ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) = ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x))

Tactic:
ext1 f

Result:
case h
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
f : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)
⊢ f ∈ nonunits ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) ↔ f ∈ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x))

Proof state:
case h
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
f : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)
⊢ IsUnit f ↔ f ∉ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x))

Tactic:
apply smoothSheafCommRing.isUnit_stalk_iff

Result:
no goals

Proof state:
case h
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
f : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)
⊢ f ∈ nonunits ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x) ↔ f ∈ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x))

Tactic:
rw [mem_nonunits_iff, not_iff_comm, Iff.comm]

Result:
case h
𝕜 : Type u
inst✝⁵ : NontriviallyNormedField 𝕜
EM : Type u_1
inst✝⁴ : NormedAddCommGroup EM
inst✝³ : NormedSpace 𝕜 EM
HM : Type u_2
inst✝² : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
M : Type u
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace HM M
x : M
f : ↑((smoothSheafCommRing IM 𝓘(𝕜, 𝕜) M 𝕜).presheaf.stalk x)
⊢ IsUnit f ↔ f ∉ ↑(RingHom.ker (eval IM 𝓘(𝕜, 𝕜) M 𝕜 x))
-- Mathlib/CategoryTheory/Limits/HasLimits.lean
theorem colimit.eqToHom_comp_ι (F : J ⥤ C) [HasColimit F] {j j' : J} (hj : j = j') :
    eqToHom (by subst hj; rfl) ≫ colimit.ι F j = colimit.ι F j'

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimit F
j j' : J
hj : j = j'
⊢ eqToHom ⋯ ≫ ι F j = ι F j'

Tactic:
subst hj

Result:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimit F
j : J
⊢ eqToHom ⋯ ≫ ι F j = ι F j

Proof state:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasColimit F
j : J
⊢ F.obj j = F.obj j

Tactic:
rfl

Result:
no goals

Proof state:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
C : Type u
inst✝¹ : Category.{v, u} C
F : J ⥤ C
inst✝ : HasColimit F
j : J
⊢ eqToHom ⋯ ≫ ι F j = ι F j

Tactic:
simp

Result:
no goals

Proof state:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasColimit F
j j' : J
hj : j = j'
⊢ F.obj j' = F.obj j

Tactic:
subst hj

Result:
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u
inst✝¹ : Category.{v, u} C
F✝ F : J ⥤ C
inst✝ : HasColimit F
j : J
⊢ F.obj j = F.obj j
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem norm_normComp : ‖f.normComp‖ = ‖f‖

Proof state:
α : Type u
β : Type v
inst✝¹ : TopologicalSpace α
inst✝ : SeminormedAddCommGroup β
f : α →ᵇ β
⊢ ‖f.normComp‖ = ‖f‖

Tactic:
simp only [norm_eq, coe_normComp, norm_norm, Function.comp]

Result:
no goals