harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_int_le_pow_iff_dvd (k : ℤ) (n : ℕ) :
    ‖(k : ℚ_[p])‖ ≤ (p : ℝ) ^ (-n : ℤ) ↔ (p ^ n : ℤ) ∣ k

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑↑p ^ (-↑n)
⊢ ↑k = ↑↑k

Tactic:
norm_cast

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑↑p ^ (-↑n)
⊢ ↑(padicNorm p ↑k) ≤ ↑↑p ^ (-↑n) ↔ ↑p ^ n ∣ k

Tactic:
norm_cast

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑↑p ^ (-↑n)
⊢ padicNorm p ↑k ≤ ↑p ^ (-↑n) ↔ ↑(p ^ n) ∣ k

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
⊢ ↑p ^ (-↑n) = ↑↑p ^ (-↑n)

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
⊢ ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k

Tactic:
have : (p : ℝ) ^ (-n : ℤ) = (p : ℚ) ^ (-n : ℤ) := by simp

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑↑p ^ (-↑n)
⊢ ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑↑p ^ (-↑n)
⊢ ‖↑k‖ ≤ ↑p ^ (-↑n) ↔ ↑p ^ n ∣ k

Tactic:
rw [show (k : ℚ_[p]) = ((k : ℚ) : ℚ_[p]) by norm_cast, eq_padicNorm, this]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑↑p ^ (-↑n)
⊢ ↑(padicNorm p ↑k) ≤ ↑↑p ^ (-↑n) ↔ ↑p ^ n ∣ k

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
n : ℕ
this : ↑p ^ (-↑n) = ↑↑p ^ (-↑n)
⊢ padicNorm p ↑k ≤ ↑p ^ (-↑n) ↔ ↑(p ^ n) ∣ k

Tactic:
rw [← padicNorm.dvd_iff_norm_le]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean
@[reassoc (attr := simp)]
lemma biprod_lift_fst_f (α : M ⟶ K) (β : M ⟶ L) (i : ι) :
    (biprod.lift α β).f i ≫ (biprod.fst : K ⊞ L ⟶ K).f i = α.f i

Proof state:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
M : HomologicalComplex C c
α : M ⟶ K
β : M ⟶ L
i : ι
⊢ (biprod.lift α β).f i ≫ biprod.fst.f i = α.f i

Tactic:
rw [← comp_f, biprod.lift_fst]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem self_le_toNat (a : Int) : a ≤ toNat a

Proof state:
a : Int
⊢ a ≤ ↑a.toNat

Tactic:
rw [toNat_eq_max]

Result:
a : Int
⊢ a ≤ max a 0

Proof state:
a : Int
⊢ a ≤ max a 0

Tactic:
apply Int.le_max_left

Result:
no goals
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem exists_upperCrossingTime_eq (f : ℕ → Ω → ℝ) (N : ℕ) (ω : Ω) (hab : a < b) :
    ∃ n, upperCrossingTime a b f N n ω = N

Proof state:
case intro.intro.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N
this : StrictMono fun n => upperCrossingTime a b f N n ω
k : ℕ
hk : N < (fun n => upperCrossingTime a b f N n ω) k
⊢ False

Tactic:
exact not_le.2 hk upperCrossingTime_le

Result:
no goals

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ¬∃ n, upperCrossingTime a b f N n ω = N
⊢ False

Tactic:
push_neg at h

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N
⊢ False

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N
⊢ False

Tactic:
have : StrictMono fun n => upperCrossingTime a b f N n ω :=
  strictMono_nat_of_lt_succ fun n => upperCrossingTime_lt_succ hab (h _)

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N
this : StrictMono fun n => upperCrossingTime a b f N n ω
⊢ False

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
⊢ ∃ n, upperCrossingTime a b f N n ω = N

Tactic:
by_contra h

Result:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ¬∃ n, upperCrossingTime a b f N n ω = N
⊢ False

Proof state:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N
this : StrictMono fun n => upperCrossingTime a b f N n ω
⊢ False

Tactic:
obtain ⟨_, ⟨k, rfl⟩, hk⟩ :
    ∃ (m : _) (_ : m ∈ Set.range fun n => upperCrossingTime a b f N n ω), N < m :=
  ⟨upperCrossingTime a b f N (N + 1) ω, ⟨N + 1, rfl⟩,
    lt_of_lt_of_le N.lt_succ_self (StrictMono.id_le this (N + 1))⟩

Result:
case intro.intro.intro
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N
this : StrictMono fun n => upperCrossingTime a b f N n ω
k : ℕ
hk : N < (fun n => upperCrossingTime a b f N n ω) k
⊢ False
-- Mathlib/Analysis/Matrix.lean
theorem nnnorm_col (v : m → α) : ‖col ι v‖₊ = ‖v‖₊

Proof state:
m : Type u_3
α : Type u_5
ι : Type u_7
inst✝² : Fintype m
inst✝¹ : Unique ι
inst✝ : SeminormedAddCommGroup α
v : m → α
⊢ ‖col ι v‖₊ = ‖v‖₊

Tactic:
simp [nnnorm_def, Pi.nnnorm_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem findRev?_eq_find?_reverse (f : α → Bool) (as : Array α) :
    as.findRev? f = as.reverse.find? f

Proof state:
α : Type
f : α → Bool
as : Array α
⊢ findRev? f as = find? f as.reverse

Tactic:
cases as

Result:
case mk
α : Type
f : α → Bool
toList✝ : List α
⊢ findRev? f { toList := toList✝ } = find? f { toList := toList✝ }.reverse

Proof state:
case mk
α : Type
f : α → Bool
toList✝ : List α
⊢ findRev? f { toList := toList✝ } = find? f { toList := toList✝ }.reverse

Tactic:
simp [findRev?, Id.run]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_eq_getMsb?_getD (x : BitVec w) (i : Nat) :
    x.getMsbD i = (x.getMsb? i).getD false

Proof state:
case pos
w : Nat
x : BitVec w
i : Nat
h : w = 0
⊢ (decide (i < w) && x.getLsbD (w - 1 - i)) = (x.getMsb? i).getD false

Tactic:
simp [getMsb?, h]

Result:
no goals

Proof state:
case neg
w : Nat
x : BitVec w
i : Nat
h : ¬w = 0
⊢ (decide (i < w) && x.getLsbD (w - 1 - i)) = (x.getMsb? i).getD false

Tactic:
rw [getLsbD_eq_getElem?_getD, getMsb?_eq_getLsb?]

Result:
case neg
w : Nat
x : BitVec w
i : Nat
h : ¬w = 0
⊢ (decide (i < w) && x[w - 1 - i]?.getD false) = (if i < w then x.getLsb? (w - 1 - i) else none).getD false

Proof state:
case neg.isFalse
w : Nat
x : BitVec w
i : Nat
h : ¬w = 0
h✝ : ¬i < w
⊢ i < w → x[w - 1 - i]?.getD false = false

Tactic:
intros

Result:
case neg.isFalse
w : Nat
x : BitVec w
i : Nat
h : ¬w = 0
h✝ : ¬i < w
a✝ : i < w
⊢ x[w - 1 - i]?.getD false = false

Proof state:
case neg.isFalse
w : Nat
x : BitVec w
i : Nat
h : ¬w = 0
h✝ : ¬i < w
a✝ : i < w
⊢ x[w - 1 - i]?.getD false = false

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ (decide (i < w) && x.getLsbD (w - 1 - i)) = (x.getMsb? i).getD false

Tactic:
by_cases h : w = 0

Result:
case pos
w : Nat
x : BitVec w
i : Nat
h : w = 0
⊢ (decide (i < w) && x.getLsbD (w - 1 - i)) = (x.getMsb? i).getD false

case neg
w : Nat
x : BitVec w
i : Nat
h : ¬w = 0
⊢ (decide (i < w) && x.getLsbD (w - 1 - i)) = (x.getMsb? i).getD false

Proof state:
case neg.isFalse
w : Nat
x : BitVec w
i : Nat
h : ¬w = 0
h✝ : ¬i < w
⊢ (decide (i < w) && x[w - 1 - i]?.getD false) = none.getD false

Tactic:
simp only [getLsb?_eq_getElem?, Bool.and_iff_right_iff_imp, decide_eq_true_eq,
  Option.getD_none, Bool.and_eq_false_imp]

Result:
case neg.isFalse
w : Nat
x : BitVec w
i : Nat
h : ¬w = 0
h✝ : ¬i < w
⊢ i < w → x[w - 1 - i]?.getD false = false

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ x.getMsbD i = (x.getMsb? i).getD false

Tactic:
rw [getMsbD_eq_getLsbD]

Result:
w : Nat
x : BitVec w
i : Nat
⊢ (decide (i < w) && x.getLsbD (w - 1 - i)) = (x.getMsb? i).getD false
-- Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
theorem of_aeval {f : ι → MvPolynomial ι R}
    (H : AlgebraicIndependent R fun i ↦ aeval x (f i)) :
    AlgebraicIndependent R f

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → MvPolynomial ι R
H : ∀ (p : MvPolynomial ι R), (aeval fun i => (aeval x) (f i)) p = 0 → p = 0
⊢ ∀ (p : MvPolynomial ι R), (aeval f) p = 0 → p = 0

Tactic:
intro p hp

Result:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → MvPolynomial ι R
H : ∀ (p : MvPolynomial ι R), (aeval fun i => (aeval x) (f i)) p = 0 → p = 0
p : MvPolynomial ι R
hp : (aeval f) p = 0
⊢ p = 0

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → MvPolynomial ι R
H : ∀ (p : MvPolynomial ι R), (aeval fun i => (aeval x) (f i)) p = 0 → p = 0
p : MvPolynomial ι R
hp : (aeval f) p = 0
⊢ (aeval fun i => (aeval x) (f i)) p = 0

Tactic:
rw [← aeval_comp_bind₁, AlgHom.comp_apply, bind₁, hp, map_zero]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → MvPolynomial ι R
H : ∀ (p : MvPolynomial ι R), (aeval fun i => (aeval x) (f i)) p = 0 → p = 0
p : MvPolynomial ι R
hp : (aeval f) p = 0
⊢ p = 0

Tactic:
exact H p (by rw [← aeval_comp_bind₁, AlgHom.comp_apply, bind₁, hp, map_zero])

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → MvPolynomial ι R
H : AlgebraicIndependent R fun i => (aeval x) (f i)
⊢ AlgebraicIndependent R f

Tactic:
rw [algebraicIndependent_iff] at H ⊢

Result:
ι : Type u_1
R : Type u_3
A : Type u_5
x : ι → A
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : ι → MvPolynomial ι R
H : ∀ (p : MvPolynomial ι R), (aeval fun i => (aeval x) (f i)) p = 0 → p = 0
⊢ ∀ (p : MvPolynomial ι R), (aeval f) p = 0 → p = 0
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem lt_inf {a b c : CauSeq α abs} (hb : a < b) (hc : a < c) : a < b ⊓ c

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ ↑(b - a) j
εc : α
εc0 : εc > 0
ic : ℕ
hc : ∀ j ≥ ic, εc ≤ ↑(c - a) j
⊢ a < b ⊓ c

Tactic:
refine ⟨εb ⊓ εc, lt_inf_iff.mpr ⟨εb0, εc0⟩, ib ⊔ ic, fun i hi => ?_⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ ↑(b - a) j
εc : α
εc0 : εc > 0
ic : ℕ
hc : ∀ j ≥ ic, εc ≤ ↑(c - a) j
i : ℕ
hi : i ≥ ib ⊔ ic
⊢ εb ⊓ εc ≤ ↑(b ⊓ c - a) i

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ ↑(b - a) j
εc : α
εc0 : εc > 0
ic : ℕ
hc : ∀ j ≥ ic, εc ≤ ↑(c - a) j
i : ℕ
hi : i ≥ ib ⊔ ic
⊢ εb ⊓ εc ≤ ↑(b ⊓ c - a) i

Tactic:
have := min_le_min (hb _ (sup_le_iff.mp hi).1) (hc _ (sup_le_iff.mp hi).2)

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ ↑(b - a) j
εc : α
εc0 : εc > 0
ic : ℕ
hc : ∀ j ≥ ic, εc ≤ ↑(c - a) j
i : ℕ
hi : i ≥ ib ⊔ ic
this : εb ⊓ εc ≤ ↑(b - a) i ⊓ ↑(c - a) i
⊢ εb ⊓ εc ≤ ↑(b ⊓ c - a) i

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ ↑(b - a) j
εc : α
εc0 : εc > 0
ic : ℕ
hc : ∀ j ≥ ic, εc ≤ ↑(c - a) j
i : ℕ
hi : i ≥ ib ⊔ ic
this : εb ⊓ εc ≤ ↑(b - a) i ⊓ ↑(c - a) i
⊢ εb ⊓ εc ≤ ↑(b ⊓ c - a) i

Tactic:
exact this.trans_eq (min_sub_sub_right _ _ _)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
hb : a < b
hc : a < c
⊢ a < b ⊓ c

Tactic:
obtain ⟨⟨εb, εb0, ib, hb⟩, ⟨εc, εc0, ic, hc⟩⟩ := hb, hc

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : LinearOrderedField α
a b c : CauSeq α abs
εb : α
εb0 : εb > 0
ib : ℕ
hb : ∀ j ≥ ib, εb ≤ ↑(b - a) j
εc : α
εc0 : εc > 0
ic : ℕ
hc : ∀ j ≥ ic, εc ≤ ↑(c - a) j
⊢ a < b ⊓ c
-- Mathlib/Combinatorics/SimpleGraph/Coloring.lean
theorem chromaticNumber_le_one_of_subsingleton (G : SimpleGraph V) [Subsingleton V] :
    G.chromaticNumber ≤ 1

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ ∀ {v w : V}, G.Adj v w → (fun x => 0) v ≠ (fun x => 0) w

Tactic:
intros v w

Result:
V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
v w : V
⊢ G.Adj v w → (fun x => 0) v ≠ (fun x => 0) w

Proof state:
case refl
V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
v : V
⊢ G.Adj v v → (fun x => 0) v ≠ (fun x => 0) v

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ G.chromaticNumber ≤ 1

Tactic:
rw [← Nat.cast_one, chromaticNumber_le_iff_colorable]

Result:
V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ G.Colorable 1

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ G.Colorable 1

Tactic:
refine ⟨Coloring.mk (fun _ => 0) ?_⟩

Result:
V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
⊢ ∀ {v w : V}, G.Adj v w → (fun x => 0) v ≠ (fun x => 0) w

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
v w : V
⊢ G.Adj v w → (fun x => 0) v ≠ (fun x => 0) w

Tactic:
cases Subsingleton.elim v w

Result:
case refl
V : Type u
G : SimpleGraph V
inst✝ : Subsingleton V
v : V
⊢ G.Adj v v → (fun x => 0) v ≠ (fun x => 0) v
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem weightedHomogeneousSubmodule_eq_finsupp_supported (w : σ → M) (m : M) :
    weightedHomogeneousSubmodule R w m = Finsupp.supported R R { d | weight w d = m }

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
⊢ weightedHomogeneousSubmodule R w m = supported R R {d | (weight w) d = m}

Tactic:
ext x

Result:
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
x : MvPolynomial σ R
⊢ x ∈ weightedHomogeneousSubmodule R w m ↔ x ∈ supported R R {d | (weight w) d = m}

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
x : MvPolynomial σ R
⊢ x ∈ weightedHomogeneousSubmodule R w m ↔ ∀ (x_1 : σ →₀ ℕ), x x_1 ≠ 0 → x_1 ∈ {d | (weight w) d = m}

Tactic:
rfl

Result:
no goals

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
x : MvPolynomial σ R
⊢ x ∈ weightedHomogeneousSubmodule R w m ↔ x ∈ supported R R {d | (weight w) d = m}

Tactic:
rw [mem_supported, Set.subset_def]

Result:
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
x : MvPolynomial σ R
⊢ x ∈ weightedHomogeneousSubmodule R w m ↔ ∀ x_1 ∈ ↑x.support, x_1 ∈ {d | (weight w) d = m}

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
x : MvPolynomial σ R
⊢ x ∈ weightedHomogeneousSubmodule R w m ↔ ∀ x_1 ∈ ↑x.support, x_1 ∈ {d | (weight w) d = m}

Tactic:
simp only [Finsupp.mem_support_iff, mem_coe]

Result:
case h
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
x : MvPolynomial σ R
⊢ x ∈ weightedHomogeneousSubmodule R w m ↔ ∀ (x_1 : σ →₀ ℕ), x x_1 ≠ 0 → x_1 ∈ {d | (weight w) d = m}
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
/-- The upper part of the third column of the snake diagram is exact. -/
lemma exact_C₃_up : (ShortComplex.mk S.v₀₁.τ₃ S.v₁₂.τ₃
    (by rw [← comp_τ₃, S.w₀₂, zero_τ₃])).Exact :=
  exact_of_f_is_kernel _ S.h₀τ₃

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.32090, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.v₀₁.τ₃ ≫ S.v₁₂.τ₃ = 0

Tactic:
rw [← comp_τ₃, S.w₀₂, zero_τ₃]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem flatMap_cons x xs (f : α → List β) :
  List.flatMap f (x :: xs) = f x ++ List.flatMap f xs

Proof state:
α : Type u
β : Type v
x : α
xs : List α
f : α → List β
⊢ flatMap f (x :: xs) = f x ++ flatMap f xs

Tactic:
simp [flatten, List.flatMap]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
@[to_additive]
lemma mul_le_prod {i j : ι} (hf : ∀ i ∈ s, 1 ≤ f i) (hi : i ∈ s) (hj : j ∈ s) (hne : i ≠ j) :
    f i * f j ≤ ∏ k ∈ s, f k :=
  calc
    f i * f j = ∏ k ∈ .cons i {j} (by simpa), f k

Proof state:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s : Finset ι
i j : ι
hf : ∀ i ∈ s, 1 ≤ f i
hi : i ∈ s
hj : j ∈ s
hne : i ≠ j
⊢ i ∉ {j}

Tactic:
simpa

Result:
no goals

Proof state:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s : Finset ι
i j : ι
hf : ∀ i ∈ s, 1 ≤ f i
hi : i ∈ s
hj : j ∈ s
hne : i ≠ j
⊢ f i * f j = ∏ k ∈ cons i {j} ⋯, f k

Tactic:
rw [prod_cons, prod_singleton]

Result:
no goals

Proof state:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s : Finset ι
i j : ι
hf : ∀ i ∈ s, 1 ≤ f i
hi : i ∈ s
hj : j ∈ s
hne : i ≠ j
⊢ cons i {j} ⋯ ⊆ s

Tactic:
simp [cons_subset, *]

Result:
no goals

Proof state:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s : Finset ι
i j : ι
hf : ∀ i ∈ s, 1 ≤ f i
hi : i ∈ s
hj : j ∈ s
hne : i ≠ j
⊢ ∏ k ∈ cons i {j} ⋯, f k ≤ ∏ k ∈ s, f k

Tactic:
refine prod_le_prod_of_subset_of_one_le' ?_ fun k hk _ ↦ hf k hk

Result:
ι : Type u_1
N : Type u_5
inst✝ : OrderedCommMonoid N
f : ι → N
s : Finset ι
i j : ι
hf : ∀ i ∈ s, 1 ≤ f i
hi : i ∈ s
hj : j ∈ s
hne : i ≠ j
⊢ cons i {j} ⋯ ⊆ s
-- Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
theorem r_pow (i : ZMod n) (k : ℕ) : (r i)^k = r (i * k : ZMod n)

Proof state:
case zero
n : ℕ
i : ZMod n
⊢ r i ^ 0 = r (i * ↑0)

Tactic:
simp only [pow_zero, Nat.cast_zero, mul_zero, r_zero]

Result:
no goals

Proof state:
case succ
n : ℕ
i : ZMod n
k : ℕ
IH : r i ^ k = r (i * ↑k)
⊢ r i ^ (k + 1) = r (i * ↑(k + 1))

Tactic:
rw [pow_add, pow_one, IH, r_mul_r, Nat.cast_add, Nat.cast_one, r.injEq, mul_add, mul_one]

Result:
no goals

Proof state:
n : ℕ
i : ZMod n
k : ℕ
⊢ r i ^ k = r (i * ↑k)

Tactic:
induction k with
| zero => simp only [pow_zero, Nat.cast_zero, mul_zero, r_zero]
| succ k IH =>
  rw [pow_add, pow_one, IH, r_mul_r, Nat.cast_add, Nat.cast_one, r.injEq, mul_add, mul_one]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
@[simp] lemma div_pos_iff_of_pos_left (ha : 0 < a) : 0 < a / b ↔ 0 < b

Proof state:
α : Type u_2
inst✝ : LinearOrderedSemifield α
a b : α
ha : 0 < a
⊢ 0 < a / b ↔ 0 < b

Tactic:
simp only [div_eq_mul_inv, mul_pos_iff_of_pos_left ha, inv_pos]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Matrix.lean
lemma l2_opNorm_conjTranspose_mul_self (A : Matrix m n 𝕜) : ‖Aᴴ * A‖ = ‖A‖ * ‖A‖

Proof state:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ‖Aᴴ * A‖ = ‖A‖ * ‖A‖

Tactic:
classical
rw [l2_opNorm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
  Matrix.toLin_mul (v₂ := (EuclideanSpace.basisFun m 𝕜).toBasis), toLin_conjTranspose]
exact ContinuousLinearMap.norm_adjoint_comp_self _

Result:
no goals

Proof state:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ‖toContinuousLinearMap
        (adjoint ((toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis) A) ∘ₗ
          (toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis) A)‖ =
    ‖A‖ * ‖A‖

Tactic:
exact ContinuousLinearMap.norm_adjoint_comp_self _

Result:
no goals

Proof state:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ‖Aᴴ * A‖ = ‖A‖ * ‖A‖

Tactic:
rw [l2_opNorm_def, toEuclideanLin_eq_toLin_orthonormal, LinearEquiv.trans_apply,
  Matrix.toLin_mul (v₂ := (EuclideanSpace.basisFun m 𝕜).toBasis), toLin_conjTranspose]

Result:
𝕜 : Type u_1
m : Type u_2
n : Type u_3
inst✝³ : RCLike 𝕜
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix m n 𝕜
⊢ ‖toContinuousLinearMap
        (adjoint ((toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis) A) ∘ₗ
          (toLin (EuclideanSpace.basisFun n 𝕜).toBasis (EuclideanSpace.basisFun m 𝕜).toBasis) A)‖ =
    ‖A‖ * ‖A‖
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem is3Clique_iff_exists_cycle_length_three :
    (∃ s : Finset α, G.IsNClique 3 s) ↔ ∃ (u : α) (w : G.Walk u u), w.IsCycle ∧ w.length = 3

Proof state:
α : Type u_1
G : SimpleGraph α
⊢ (∃ s, G.IsNClique 3 s) ↔ ∃ u w, w.IsCycle ∧ w.length = 3

Tactic:
classical
simp_rw [is3Clique_iff, isCycle_def]
exact
  ⟨(fun ⟨_, a, _, _, hab, hac, hbc, _⟩ => ⟨a, cons hab (cons hbc (cons hac.symm nil)), by aesop⟩),
  (fun ⟨_, .cons hab (.cons hbc (.cons hca nil)), _, _⟩ => ⟨_, _, _, _, hab, hca.symm, hbc, rfl⟩)⟩

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
⊢ (∃ s, G.IsNClique 3 s) ↔ ∃ u w, w.IsCycle ∧ w.length = 3

Tactic:
simp_rw [is3Clique_iff, isCycle_def]

Result:
α : Type u_1
G : SimpleGraph α
⊢ (∃ s a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ↔
    ∃ u w, (w.IsTrail ∧ w ≠ nil ∧ w.support.tail.Nodup) ∧ w.length = 3

Proof state:
α : Type u_1
G : SimpleGraph α
x✝ : ∃ s a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}
w✝² : Finset α
a w✝¹ w✝ : α
hab : G.Adj a w✝¹
hac : G.Adj a w✝
hbc : G.Adj w✝¹ w✝
right✝ : w✝² = {a, w✝¹, w✝}
⊢ ((Walk.cons hab (Walk.cons hbc (Walk.cons ⋯ nil))).IsTrail ∧
      Walk.cons hab (Walk.cons hbc (Walk.cons ⋯ nil)) ≠ nil ∧
        (Walk.cons hab (Walk.cons hbc (Walk.cons ⋯ nil))).support.tail.Nodup) ∧
    (Walk.cons hab (Walk.cons hbc (Walk.cons ⋯ nil))).length = 3

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
⊢ (∃ s a b c, G.Adj a b ∧ G.Adj a c ∧ G.Adj b c ∧ s = {a, b, c}) ↔
    ∃ u w, (w.IsTrail ∧ w ≠ nil ∧ w.support.tail.Nodup) ∧ w.length = 3

Tactic:
exact
  ⟨(fun ⟨_, a, _, _, hab, hac, hbc, _⟩ => ⟨a, cons hab (cons hbc (cons hac.symm nil)), by aesop⟩),
  (fun ⟨_, .cons hab (.cons hbc (.cons hca nil)), _, _⟩ => ⟨_, _, _, _, hab, hca.symm, hbc, rfl⟩)⟩

Result:
no goals
-- Mathlib/CategoryTheory/Yoneda.lean
lemma yonedaEquiv_yoneda_map {X Y : C} (f : X ⟶ Y) : yonedaEquiv (yoneda.map f) = f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ yonedaEquiv (yoneda.map f) = f

Tactic:
rw [yonedaEquiv_apply]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (yoneda.map f).app (op X) (𝟙 X) = f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
⊢ (yoneda.map f).app (op X) (𝟙 X) = f

Tactic:
simp

Result:
no goals
-- Mathlib/Data/PNat/Basic.lean
theorem mul_div_exact {m k : ℕ+} (h : k ∣ m) : k * divExact m k = m

Proof state:
case a
m k : ℕ+
h : k ∣ m
⊢ ↑(k * m.divExact k) = ↑m

Tactic:
rw [mul_coe]

Result:
case a
m k : ℕ+
h : k ∣ m
⊢ ↑k * ↑(m.divExact k) = ↑m

Proof state:
case a
m k : ℕ+
h : k ∣ m
⊢ ↑k * (m.div k).succ = ↑m

Tactic:
rw [← div_add_mod m k, dvd_iff'.mp h, Nat.mul_succ]

Result:
no goals

Proof state:
m k : ℕ+
h : k ∣ m
⊢ k * m.divExact k = m

Tactic:
apply PNat.eq

Result:
case a
m k : ℕ+
h : k ∣ m
⊢ ↑(k * m.divExact k) = ↑m

Proof state:
case a
m k : ℕ+
h : k ∣ m
⊢ ↑k * ↑(m.divExact k) = ↑m

Tactic:
change (k : ℕ) * (div m k).succ = m

Result:
case a
m k : ℕ+
h : k ∣ m
⊢ ↑k * (m.div k).succ = ↑m
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem _root_.Sbtw.oangle_eq_add_pi_left
    {p₁ p₁' p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₁') (hp₃p₂ : p₃ ≠ p₂) :
    ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃ + π

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₁' p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₁'
hp₃p₂ : p₃ ≠ p₂
⊢ ∡ p₁ p₂ p₃ = ∡ p₁' p₂ p₃ + ↑π

Tactic:
rw [← h.oangle₁₂₃_eq_pi, oangle_add_swap h.left_ne h.right_ne hp₃p₂]

Result:
no goals