harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Fintype/Prod.lean
theorem infinite_prod : Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β

Proof state:
α : Type u_1
β : Type u_2
H : Infinite (α × β)
⊢ Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β

Tactic:
contrapose! H

Result:
α : Type u_1
β : Type u_2
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
⊢ ¬Infinite (α × β)

Proof state:
α : Type u_1
β : Type u_2
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
⊢ False

Tactic:
rcases Infinite.nonempty (α × β) with ⟨a, b⟩

Result:
case intro.mk
α : Type u_1
β : Type u_2
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
a : α
b : β
⊢ False

Proof state:
case intro.mk
α : Type u_1
β : Type u_2
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
a : α
b : β
⊢ False

Tactic:
haveI := fintypeOfNotInfinite (H.1 ⟨b⟩)

Result:
case intro.mk
α : Type u_1
β : Type u_2
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
a : α
b : β
this : Fintype α
⊢ False

Proof state:
α : Type u_1
β : Type u_2
⊢ Infinite (α × β) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β

Tactic:
refine
  ⟨fun H => ?_, fun H =>
    H.elim (and_imp.2 <| @Prod.infinite_of_left α β) (and_imp.2 <| @Prod.infinite_of_right α β)⟩

Result:
α : Type u_1
β : Type u_2
H : Infinite (α × β)
⊢ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β

Proof state:
case intro.mk
α : Type u_1
β : Type u_2
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
a : α
b : β
this : Fintype α
⊢ False

Tactic:
haveI := fintypeOfNotInfinite (H.2 ⟨a⟩)

Result:
case intro.mk
α : Type u_1
β : Type u_2
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
a : α
b : β
this✝ : Fintype α
this : Fintype β
⊢ False

Proof state:
case intro.mk
α : Type u_1
β : Type u_2
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
a : α
b : β
this✝ : Fintype α
this : Fintype β
⊢ False

Tactic:
exact H'.false

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
⊢ ¬Infinite (α × β)

Tactic:
intro H'

Result:
α : Type u_1
β : Type u_2
H : (Nonempty β → ¬Infinite α) ∧ (Nonempty α → ¬Infinite β)
H' : Infinite (α × β)
⊢ False

Proof state:
α : Type u_1
β : Type u_2
H : Infinite (α × β)
⊢ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β

Tactic:
rw [and_comm]

Result:
α : Type u_1
β : Type u_2
H : Infinite (α × β)
⊢ Nonempty β ∧ Infinite α ∨ Nonempty α ∧ Infinite β
-- Mathlib/Order/Filter/Ker.lean
theorem ker_sSup (S : Set (Filter α)) : ker (sSup S) = ⋃ f ∈ S, ker f

Proof state:
α : Type u_2
S : Set (Filter α)
⊢ (sSup S).ker = ⋃ f ∈ S, f.ker

Tactic:
simp [sSup_eq_iSup]

Result:
no goals
-- Mathlib/CategoryTheory/Adhesive.lean
theorem IsPushout.IsVanKampen.flip {H : IsPushout f g h i} (H' : H.IsVanKampen) :
    H.flip.IsVanKampen

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' : H.IsVanKampen
⊢ ⋯.IsVanKampen

Tactic:
introv W' hf hg hh hi w

Result:
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' : H.IsVanKampen
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ Y
αY : Y' ⟶ X
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX g
hg : IsPullback g' αW αY f
hh : CommSq h' αX αZ i
hi : CommSq i' αY αZ h
w : CommSq f' g' h' i'
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ i ∧ IsPullback i' αY αZ h

Proof state:
C : Type u
inst✝ : Category.{v, u} C
W X Y Z : C
f : W ⟶ X
g : W ⟶ Y
h : X ⟶ Z
i : Y ⟶ Z
H : IsPushout f g h i
H' : H.IsVanKampen
W' X' Y' Z' : C
f' : W' ⟶ X'
g' : W' ⟶ Y'
h' : X' ⟶ Z'
i' : Y' ⟶ Z'
αW : W' ⟶ W
αX : X' ⟶ Y
αY : Y' ⟶ X
αZ : Z' ⟶ Z
hf : IsPullback f' αW αX g
hg : IsPullback g' αW αY f
hh : CommSq h' αX αZ i
hi : CommSq i' αY αZ h
w : CommSq f' g' h' i'
⊢ IsPushout f' g' h' i' ↔ IsPullback h' αX αZ i ∧ IsPullback i' αY αZ h

Tactic:
simpa only [IsPushout.flip_iff, IsPullback.flip_iff, and_comm] using
  H' g' f' i' h' αW αY αX αZ hg hf hi hh w.flip

Result:
no goals
-- Mathlib/RingTheory/FinitePresentation.lean
theorem comp_surjective {f : A →+* B} {g : B →+* C} (hf : f.FinitePresentation) (hg : Surjective g)
    (hker : g.ker.FG) : (g.comp f).FinitePresentation

Proof state:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hf : f.FinitePresentation
hg : Surjective ⇑g
hker : (ker g).FG
algInst✝¹ : Algebra A B := f.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation A B
⊢ (g.comp f).FinitePresentation

Tactic:
exact Algebra.FinitePresentation.of_surjective
  (f :=
    { g with
      toFun := g
      commutes' := fun _ => rfl })
  hg hker

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hf : f.FinitePresentation
hg : Surjective ⇑g
hker : (ker g).FG
⊢ (g.comp f).FinitePresentation

Tactic:
algebraize [f, g.comp f]

Result:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommRing A
inst✝¹ : CommRing B
inst✝ : CommRing C
f : A →+* B
g : B →+* C
hf : f.FinitePresentation
hg : Surjective ⇑g
hker : (ker g).FG
algInst✝¹ : Algebra A B := f.toAlgebra
algInst✝ : Algebra A C := (g.comp f).toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation A B
⊢ (g.comp f).FinitePresentation
-- Mathlib/LinearAlgebra/Pi.lean
theorem pi_ext' (h : ∀ i, f.comp (single R φ i) = g.comp (single R φ i)) : f = g

Proof state:
R : Type u
M : Type v
ι : Type x
inst✝⁶ : Semiring R
φ : ι → Type i
inst✝⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝⁴ : (i : ι) → Module R (φ i)
inst✝³ : DecidableEq ι
inst✝² : Finite ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ((i : ι) → φ i) →ₗ[R] M
h : ∀ (i : ι), f ∘ₗ single R φ i = g ∘ₗ single R φ i
i : ι
x : φ i
⊢ f (Pi.single i x) = g (Pi.single i x)

Tactic:
convert LinearMap.congr_fun (h i) x

Result:
no goals

Proof state:
R : Type u
M : Type v
ι : Type x
inst✝⁶ : Semiring R
φ : ι → Type i
inst✝⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝⁴ : (i : ι) → Module R (φ i)
inst✝³ : DecidableEq ι
inst✝² : Finite ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ((i : ι) → φ i) →ₗ[R] M
h : ∀ (i : ι), f ∘ₗ single R φ i = g ∘ₗ single R φ i
⊢ f = g

Tactic:
refine pi_ext fun i x => ?_

Result:
R : Type u
M : Type v
ι : Type x
inst✝⁶ : Semiring R
φ : ι → Type i
inst✝⁵ : (i : ι) → AddCommMonoid (φ i)
inst✝⁴ : (i : ι) → Module R (φ i)
inst✝³ : DecidableEq ι
inst✝² : Finite ι
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f g : ((i : ι) → φ i) →ₗ[R] M
h : ∀ (i : ι), f ∘ₗ single R φ i = g ∘ₗ single R φ i
i : ι
x : φ i
⊢ f (Pi.single i x) = g (Pi.single i x)
-- Mathlib/Data/DFinsupp/Lex.lean
theorem toLex_monotone : Monotone (@toLex (Π₀ i, α i))

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
⊢ toLex a ≤ toLex b

Tactic:
refine le_of_lt_or_eq (or_iff_not_imp_right.2 fun hne ↦ ?_)

Result:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
hne : ¬toLex a = toLex b
⊢ toLex a < toLex b

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
⊢ Monotone ⇑toLex

Tactic:
intro a b h

Result:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
⊢ toLex a ≤ toLex b

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
hne : ¬toLex a = toLex b
⊢ toLex a < toLex b

Tactic:
exact ⟨Finset.min' _ (nonempty_neLocus_iff.2 hne),
  fun j hj ↦ not_mem_neLocus.1 fun h ↦ (Finset.min'_le _ _ h).not_lt hj,
  (h _).lt_of_ne (mem_neLocus.1 <| Finset.min'_mem _ _)⟩

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝² : (i : ι) → Zero (α i)
inst✝¹ : LinearOrder ι
inst✝ : (i : ι) → PartialOrder (α i)
a b : Π₀ (i : ι), α i
h : a ≤ b
hne : ¬toLex a = toLex b
⊢ toLex a < toLex b

Tactic:
classical
exact ⟨Finset.min' _ (nonempty_neLocus_iff.2 hne),
  fun j hj ↦ not_mem_neLocus.1 fun h ↦ (Finset.min'_le _ _ h).not_lt hj,
  (h _).lt_of_ne (mem_neLocus.1 <| Finset.min'_mem _ _)⟩

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_union_congr_left {X' : Set α} (h : M.closure X = M.closure X') :
    M.closure (X ∪ Y) = M.closure (X' ∪ Y)

Proof state:
α : Type u_2
M : Matroid α
X Y X' : Set α
h : M.closure X = M.closure X'
⊢ M.closure (X ∪ Y) = M.closure (X' ∪ Y)

Tactic:
rw [← M.closure_union_closure_left_eq, h, M.closure_union_closure_left_eq]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Trim.lean
theorem eLpNorm'_trim (hm : m ≤ m0) {f : α → E} (hf : StronglyMeasurable[m] f) :
    eLpNorm' f q (μ.trim hm) = eLpNorm' f q μ

Proof state:
case e_a
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ Measurable fun a => ‖f a‖ₑ ^ q

Tactic:
refine @Measurable.pow_const _ _ _ _ _ _ _ m _ (@Measurable.coe_nnreal_ennreal _ m _ ?_) q

Result:
case e_a
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ Measurable fun a => ‖f a‖₊

Proof state:
case e_a
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ.trim hm = ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ

Tactic:
refine lintegral_trim hm ?_

Result:
case e_a
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ Measurable fun a => ‖f a‖ₑ ^ q

Proof state:
case e_a
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ Measurable fun a => ‖f a‖₊

Tactic:
apply @StronglyMeasurable.measurable

Result:
case e_a.hf
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun a => ‖f a‖₊

Proof state:
case e_a.hf
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ StronglyMeasurable fun a => ‖f a‖₊

Tactic:
exact @StronglyMeasurable.nnnorm α m _ _ _ hf

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ.trim hm) ^ (1 / q) = (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)

Tactic:
congr 1

Result:
case e_a
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ.trim hm = ∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ

Proof state:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ eLpNorm' f q (μ.trim hm) = eLpNorm' f q μ

Tactic:
simp_rw [eLpNorm']

Result:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
q : ℝ
μ : Measure α
inst✝ : NormedAddCommGroup E
hm : m ≤ m0
f : α → E
hf : StronglyMeasurable f
⊢ (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ.trim hm) ^ (1 / q) = (∫⁻ (a : α), ‖f a‖ₑ ^ q ∂μ) ^ (1 / q)
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem hasZeroObject_of_hasTerminal_object [HasZeroMorphisms C] [HasTerminal C] :
    HasZeroObject C

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
f : ⊤_ C ⟶ X
⊢ f = default

Tactic:
calc
  f = 𝟙 _ ≫ f := (Category.id_comp _).symm
  _ = 0 ≫ f := by congr!; subsingleton
  _ = 0 := zero_comp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
f : ⊤_ C ⟶ X
⊢ 𝟙 (⊤_ C) ≫ f = 0 ≫ f

Tactic:
congr!

Result:
case h.e'_6
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
f : ⊤_ C ⟶ X
⊢ 𝟙 (⊤_ C) = 0

Proof state:
case h.e'_6
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
f : ⊤_ C ⟶ X
⊢ 𝟙 (⊤_ C) = 0

Tactic:
subsingleton

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
⊢ ∀ (a : X ⟶ ⊤_ C), a = default

Tactic:
aesop_cat

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
⊢ HasZeroObject C

Tactic:
refine ⟨⟨⊤_ C, fun X => ⟨⟨⟨0⟩, fun f => ?_⟩⟩, fun X => ⟨⟨⟨0⟩, by aesop_cat⟩⟩⟩⟩

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasTerminal C
X : C
f : ⊤_ C ⟶ X
⊢ f = default
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
    (BitVec.ofNat v 1).setWidth w = BitVec.ofNat w 1

Proof state:
v w : Nat
hv : 0 < v
⊢ setWidth w 1#v = 1#w

Tactic:
ext i h

Result:
case pred
v w : Nat
hv : 0 < v
i : Nat
h : i < w
⊢ (setWidth w 1#v).getLsbD i = (1#w).getLsbD i

Proof state:
case pred
v w : Nat
hv✝ : 0 < v
i : Nat
h : i < w
hi₁ : Nat.testBit 1 i = true
hv : i = 0
⊢ i < v

Tactic:
omega

Result:
no goals

Proof state:
case pred
v w : Nat
hv : 0 < v
i : Nat
h : i < w
⊢ (setWidth w 1#v).getLsbD i = (1#w).getLsbD i

Tactic:
simp only [getLsbD_setWidth, h, decide_true, getLsbD_ofNat, Bool.true_and,
  Bool.and_iff_right_iff_imp, decide_eq_true_eq]

Result:
case pred
v w : Nat
hv : 0 < v
i : Nat
h : i < w
⊢ Nat.testBit 1 i = true → i < v

Proof state:
case pred
v w : Nat
hv : 0 < v
i : Nat
h : i < w
⊢ Nat.testBit 1 i = true → i < v

Tactic:
intros hi₁

Result:
case pred
v w : Nat
hv : 0 < v
i : Nat
h : i < w
hi₁ : Nat.testBit 1 i = true
⊢ i < v

Proof state:
case pred
v w : Nat
hv : 0 < v
i : Nat
h : i < w
hi₁ : Nat.testBit 1 i = true
⊢ i < v

Tactic:
have hv := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi₁

Result:
case pred
v w : Nat
hv✝ : 0 < v
i : Nat
h : i < w
hi₁ : Nat.testBit 1 i = true
hv : i = 0
⊢ i < v
-- Mathlib/LinearAlgebra/DirectSum/Finsupp.lean
lemma finsuppLeft_smul' (s : S) (t : (ι →₀ M) ⊗[R] N) :
    finsuppLeft R M N ι (s • t) = s • finsuppLeft R M N ι t

Proof state:
case add
R : Type u_1
inst✝⁹ : CommSemiring R
M : Type u_2
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_3
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
ι : Type u_4
inst✝⁴ : DecidableEq ι
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
s : S
x y : (ι →₀ M) ⊗[R] N
hx : (finsuppLeft R M N ι) (s • x) = s • (finsuppLeft R M N ι) x
hy : (finsuppLeft R M N ι) (s • y) = s • (finsuppLeft R M N ι) y
⊢ (finsuppLeft R M N ι) (s • (x + y)) = s • (finsuppLeft R M N ι) (x + y)

Tactic:
simp [hx, hy]

Result:
no goals

Proof state:
case tmul
R : Type u_1
inst✝⁹ : CommSemiring R
M : Type u_2
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_3
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
ι : Type u_4
inst✝⁴ : DecidableEq ι
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
s : S
p : ι →₀ M
n : N
⊢ (finsuppLeft R M N ι) (s • p ⊗ₜ[R] n) = s • (finsuppLeft R M N ι) (p ⊗ₜ[R] n)

Tactic:
ext

Result:
case tmul.h
R : Type u_1
inst✝⁹ : CommSemiring R
M : Type u_2
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_3
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
ι : Type u_4
inst✝⁴ : DecidableEq ι
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
s : S
p : ι →₀ M
n : N
a✝ : ι
⊢ ((finsuppLeft R M N ι) (s • p ⊗ₜ[R] n)) a✝ = (s • (finsuppLeft R M N ι) (p ⊗ₜ[R] n)) a✝

Proof state:
case zero
R : Type u_1
inst✝⁹ : CommSemiring R
M : Type u_2
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_3
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
ι : Type u_4
inst✝⁴ : DecidableEq ι
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
s : S
⊢ (finsuppLeft R M N ι) (s • 0) = s • (finsuppLeft R M N ι) 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁹ : CommSemiring R
M : Type u_2
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_3
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
ι : Type u_4
inst✝⁴ : DecidableEq ι
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
s : S
t : (ι →₀ M) ⊗[R] N
⊢ (finsuppLeft R M N ι) (s • t) = s • (finsuppLeft R M N ι) t

Tactic:
induction t with
| zero => simp
| add x y hx hy => simp [hx, hy]
| tmul p n => ext; simp [smul_tmul', finsuppLeft_apply_tmul_apply]

Result:
no goals

Proof state:
case tmul.h
R : Type u_1
inst✝⁹ : CommSemiring R
M : Type u_2
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
N : Type u_3
inst✝⁶ : AddCommMonoid N
inst✝⁵ : Module R N
ι : Type u_4
inst✝⁴ : DecidableEq ι
S : Type u_5
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
s : S
p : ι →₀ M
n : N
a✝ : ι
⊢ ((finsuppLeft R M N ι) (s • p ⊗ₜ[R] n)) a✝ = (s • (finsuppLeft R M N ι) (p ⊗ₜ[R] n)) a✝

Tactic:
simp [smul_tmul', finsuppLeft_apply_tmul_apply]

Result:
no goals
-- Mathlib/GroupTheory/Coprod/Basic.lean
theorem snd_comp_toProd : (MonoidHom.snd M N).comp toProd = snd

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : Monoid M
inst✝ : Monoid N
⊢ (MonoidHom.snd M N).comp toProd = snd

Tactic:
rw [← fst_prod_snd, MonoidHom.snd_comp_prod]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Lemmas.lean
lemma NormedField.tendsto_norm_zpow_nhdsNE_zero_atTop {m : ℤ} (hm : m < 0) :
    Tendsto (fun x : α ↦ ‖x ^ m‖) (𝓝[≠] 0) atTop

Proof state:
case intro
α : Type u_1
inst✝ : NormedDivisionRing α
m : ℤ
hm : -m < 0
⊢ Tendsto (fun x => ‖x ^ (-m)‖) (𝓝[≠] 0) atTop

Tactic:
rw [neg_lt_zero] at hm

Result:
case intro
α : Type u_1
inst✝ : NormedDivisionRing α
m : ℤ
hm : 0 < m
⊢ Tendsto (fun x => ‖x ^ (-m)‖) (𝓝[≠] 0) atTop

Proof state:
case intro.intro
α : Type u_1
inst✝ : NormedDivisionRing α
m : ℕ
hm : 0 < m
⊢ Tendsto (fun x => ‖x ^ (-↑m)‖) (𝓝[≠] 0) atTop

Tactic:
simp only [norm_pow, zpow_neg, zpow_natCast, ← inv_pow]

Result:
case intro.intro
α : Type u_1
inst✝ : NormedDivisionRing α
m : ℕ
hm : 0 < m
⊢ Tendsto (fun x => ‖x⁻¹‖ ^ m) (𝓝[≠] 0) atTop

Proof state:
case intro.intro
α : Type u_1
inst✝ : NormedDivisionRing α
m : ℕ
hm : 0 < m
⊢ Tendsto (fun x => ‖x⁻¹‖ ^ m) (𝓝[≠] 0) atTop

Tactic:
exact (tendsto_pow_atTop hm.ne').comp NormedField.tendsto_norm_inv_nhdsNE_zero_atTop

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝ : NormedDivisionRing α
m : ℕ
hm : 0 < ↑m
⊢ Tendsto (fun x => ‖x ^ (-↑m)‖) (𝓝[≠] 0) atTop

Tactic:
rw [Int.natCast_pos] at hm

Result:
case intro.intro
α : Type u_1
inst✝ : NormedDivisionRing α
m : ℕ
hm : 0 < m
⊢ Tendsto (fun x => ‖x ^ (-↑m)‖) (𝓝[≠] 0) atTop

Proof state:
α : Type u_1
inst✝ : NormedDivisionRing α
m : ℤ
hm : m < 0
⊢ Tendsto (fun x => ‖x ^ m‖) (𝓝[≠] 0) atTop

Tactic:
obtain ⟨m, rfl⟩ := neg_surjective m

Result:
case intro
α : Type u_1
inst✝ : NormedDivisionRing α
m : ℤ
hm : -m < 0
⊢ Tendsto (fun x => ‖x ^ (-m)‖) (𝓝[≠] 0) atTop

Proof state:
case intro
α : Type u_1
inst✝ : NormedDivisionRing α
m : ℤ
hm : 0 < m
⊢ Tendsto (fun x => ‖x ^ (-m)‖) (𝓝[≠] 0) atTop

Tactic:
lift m to ℕ using hm.le

Result:
case intro.intro
α : Type u_1
inst✝ : NormedDivisionRing α
m : ℕ
hm : 0 < ↑m
⊢ Tendsto (fun x => ‖x ^ (-↑m)‖) (𝓝[≠] 0) atTop
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_insertIfNew [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    (h : Raw.WFImp m.1) {a : α} {b : β a} : Raw.WFImp (m.insertIfNew a b).1

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ Raw.WFImp (m.insertIfNew a b).val

Tactic:
rw [insertIfNew_eq_insertIfNewₘ]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ Raw.WFImp (m.insertIfNewₘ a b).val

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ Raw.WFImp (m.insertIfNewₘ a b).val

Tactic:
exact wfImp_insertIfNewₘ h

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/Orthogonality.lean
lemma wInner_cWeight_eq_boole [Fintype G] (ψ₁ ψ₂ : AddChar G R) :
    ⟪(ψ₁ : G → R), ψ₂⟫ₙ_[R] = if ψ₁ = ψ₂ then 1 else 0

Proof state:
case neg
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
⊢ wInner cWeight ⇑ψ₁ ⇑ψ₂ = 0

Tactic:
have : ψ₁⁻¹ * ψ₂ ≠ 1 := by rwa [Ne, inv_mul_eq_one]

Result:
case neg
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
this : ψ₁⁻¹ * ψ₂ ≠ 1
⊢ wInner cWeight ⇑ψ₁ ⇑ψ₂ = 0

Proof state:
case neg
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
this : ψ₁⁻¹ * ψ₂ ≠ 1
⊢ wInner cWeight ⇑ψ₁ ⇑ψ₂ = 0

Tactic:
simp_rw [wInner_cWeight_eq_expect, RCLike.inner_apply, ← inv_apply_eq_conj]

Result:
case neg
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
this : ψ₁⁻¹ * ψ₂ ≠ 1
⊢ 𝔼 i : G, (ψ₁ i)⁻¹ * ψ₂ i = 0

Proof state:
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ₁ ψ₂ : AddChar G R
⊢ wInner cWeight ⇑ψ₁ ⇑ψ₂ = if ψ₁ = ψ₂ then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ψ₁ = ψ₂
⊢ wInner cWeight ⇑ψ₁ ⇑ψ₂ = 1

case neg
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
⊢ wInner cWeight ⇑ψ₁ ⇑ψ₂ = 0

Proof state:
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
⊢ ψ₁⁻¹ * ψ₂ ≠ 1

Tactic:
rwa [Ne, inv_mul_eq_one]

Result:
no goals

Proof state:
case neg
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ¬ψ₁ = ψ₂
this : ψ₁⁻¹ * ψ₂ ≠ 1
⊢ 𝔼 i : G, (ψ₁ i)⁻¹ * ψ₂ i = 0

Tactic:
simpa [map_neg_eq_inv] using expect_eq_zero_iff_ne_zero.2 this

Result:
no goals

Proof state:
case pos
G : Type u_1
R : Type u_3
inst✝² : AddCommGroup G
inst✝¹ : RCLike R
inst✝ : Fintype G
ψ₁ ψ₂ : AddChar G R
h : ψ₁ = ψ₂
⊢ wInner cWeight ⇑ψ₁ ⇑ψ₂ = 1

Tactic:
rw [h, wInner_cWeight_self]

Result:
no goals