harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem expand_aeval {A : Type*} [Semiring A] [Algebra R A] (p : ℕ) (P : R[X]) (r : A) :
    aeval r (expand R p P) = aeval (r ^ p) P

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
a : R
⊢ (aeval r) ((expand R p) (C a)) = (aeval (r ^ p)) (C a)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
f g : R[X]
hf : (aeval r) ((expand R p) f) = (aeval (r ^ p)) f
hg : (aeval r) ((expand R p) g) = (aeval (r ^ p)) g
⊢ (aeval r) ((expand R p) (f + g)) = (aeval (r ^ p)) (f + g)

Tactic:
rw [map_add, aeval_add, aeval_add, hf, hg]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
⊢ (aeval r) ((expand R p) P) = (aeval (r ^ p)) P

Tactic:
refine Polynomial.induction_on P (fun a => by simp) (fun f g hf hg => ?_) fun n a _ => by simp

Result:
R : Type u
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
f g : R[X]
hf : (aeval r) ((expand R p) f) = (aeval (r ^ p)) f
hg : (aeval r) ((expand R p) g) = (aeval (r ^ p)) g
⊢ (aeval r) ((expand R p) (f + g)) = (aeval (r ^ p)) (f + g)

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
p : ℕ
P : R[X]
r : A
n : ℕ
a : R
x✝ : (aeval r) ((expand R p) (C a * X ^ n)) = (aeval (r ^ p)) (C a * X ^ n)
⊢ (aeval r) ((expand R p) (C a * X ^ (n + 1))) = (aeval (r ^ p)) (C a * X ^ (n + 1))

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToSimpleFunc_congr' (T : Set α → E →L[ℝ] F) (h_add : FinMeasAdditive μ T) {f g : α →ₛ E}
    (hf : Integrable f μ) (hg : Integrable g μ)
    (h : Pairwise fun x y => T (f ⁻¹' {x} ∩ g ⁻¹' {y}) = 0) :
    f.setToSimpleFunc T = g.setToSimpleFunc T :=
  show ((pair f g).map Prod.fst).setToSimpleFunc T = ((pair f g).map Prod.snd).setToSimpleFunc T by
    have h_pair : Integrable (f.pair g) μ := integrable_pair hf hg
    rw [map_setToSimpleFunc T h_add h_pair Prod.fst_zero]
    rw [map_setToSimpleFunc T h_add h_pair Prod.snd_zero]
    refine Finset.sum_congr rfl fun p hp => ?_
    rcases mem_range.1 hp with ⟨a, rfl⟩
    by_cases eq : f a = g a
    · dsimp only [pair_apply]; rw [eq]
    · have : T (pair f g ⁻¹' {(f a, g a)}) = 0

Proof state:
case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
h : Pairwise fun x y => T (⇑f ⁻¹' {x} ∩ ⇑g ⁻¹' {y}) = 0
h_pair : Integrable (⇑(f.pair g)) μ
a : α
hp : (f.pair g) a ∈ (f.pair g).range
eq : ¬f a = g a
⊢ (T (⇑(f.pair g) ⁻¹' {(f.pair g) a})) ((f.pair g) a).1 = (T (⇑(f.pair g) ⁻¹' {(f.pair g) a})) ((f.pair g) a).2

Tactic:
have : T (pair f g ⁻¹' {(f a, g a)}) = 0 := by
  have h_eq : T ((⇑(f.pair g)) ⁻¹' {(f a, g a)}) = T (f ⁻¹' {f a} ∩ g ⁻¹' {g a}) := by
    congr; rw [pair_preimage_singleton f g]
  rw [h_eq]
  exact h eq

Result:
case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f g : α →ₛ E
hf : Integrable (⇑f) μ
hg : Integrable (⇑g) μ
h : Pairwise fun x y => T (⇑f ⁻¹' {x} ∩ ⇑g ⁻¹' {y}) = 0
h_pair : Integrable (⇑(f.pair g)) μ
a : α
hp : (f.pair g) a ∈ (f.pair g).range
eq : ¬f a = g a
this : T (⇑(f.pair g) ⁻¹' {(f a, g a)}) = 0
⊢ (T (⇑(f.pair g) ⁻¹' {(f.pair g) a})) ((f.pair g) a).1 = (T (⇑(f.pair g) ⁻¹' {(f.pair g) a})) ((f.pair g) a).2
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem allOnes_le_iff {x : BitVec w} : allOnes w ≤ x ↔ x = allOnes w

Proof state:
w : Nat
x : BitVec w
⊢ allOnes w ≤ x ↔ x = allOnes w

Tactic:
constructor

Result:
case mp
w : Nat
x : BitVec w
⊢ allOnes w ≤ x → x = allOnes w

case mpr
w : Nat
x : BitVec w
⊢ x = allOnes w → allOnes w ≤ x

Proof state:
case mpr
w : Nat
x : BitVec w
⊢ x = allOnes w → allOnes w ≤ x

Tactic:
simp_all

Result:
no goals

Proof state:
case mp
w : Nat
x : BitVec w
h : allOnes w ≤ x
this : x ≤ allOnes w
⊢ x = allOnes w

Tactic:
exact Eq.symm (BitVec.le_antisymm h this)

Result:
no goals

Proof state:
case mp
w : Nat
x : BitVec w
h : allOnes w ≤ x
⊢ x = allOnes w

Tactic:
have : x ≤ allOnes w := not_lt_iff_le.mp not_allOnes_lt

Result:
case mp
w : Nat
x : BitVec w
h : allOnes w ≤ x
this : x ≤ allOnes w
⊢ x = allOnes w

Proof state:
case mp
w : Nat
x : BitVec w
⊢ allOnes w ≤ x → x = allOnes w

Tactic:
intro h

Result:
case mp
w : Nat
x : BitVec w
h : allOnes w ≤ x
⊢ x = allOnes w
-- Mathlib/FieldTheory/Minpoly/Field.lean
theorem prime (hx : IsIntegral A x) : Prime (minpoly A x)

Proof state:
case intro
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
this : (Polynomial.aeval x) p = 0 ∨ (Polynomial.aeval x) q = 0
⊢ minpoly A x ∣ p ∨ minpoly A x ∣ q

Tactic:
exact Or.imp (dvd A x) (dvd A x) this

Result:
no goals

Proof state:
case intro
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
⊢ minpoly A x ∣ p ∨ minpoly A x ∣ q

Tactic:
have : Polynomial.aeval x (p * q) = 0 := by simp [h, aeval A x]

Result:
case intro
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
this : (Polynomial.aeval x) (p * q) = 0
⊢ minpoly A x ∣ p ∨ minpoly A x ∣ q

Proof state:
case intro
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
this : (Polynomial.aeval x) (p * q) = 0
⊢ minpoly A x ∣ p ∨ minpoly A x ∣ q

Tactic:
replace : Polynomial.aeval x p = 0 ∨ Polynomial.aeval x q = 0 := by simpa

Result:
case intro
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
this : (Polynomial.aeval x) p = 0 ∨ (Polynomial.aeval x) q = 0
⊢ minpoly A x ∣ p ∨ minpoly A x ∣ q

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ ∀ (a b : A[X]), minpoly A x ∣ a * b → minpoly A x ∣ a ∨ minpoly A x ∣ b

Tactic:
rintro p q ⟨d, h⟩

Result:
case intro
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
⊢ minpoly A x ∣ p ∨ minpoly A x ∣ q

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
this : (Polynomial.aeval x) (p * q) = 0
⊢ (Polynomial.aeval x) p = 0 ∨ (Polynomial.aeval x) q = 0

Tactic:
simpa

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ Prime (minpoly A x)

Tactic:
refine ⟨minpoly.ne_zero hx, not_isUnit A x, ?_⟩

Result:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ ∀ (a b : A[X]), minpoly A x ∣ a * b → minpoly A x ∣ a ∨ minpoly A x ∣ b

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
p q d : A[X]
h : p * q = minpoly A x * d
⊢ (Polynomial.aeval x) (p * q) = 0

Tactic:
simp [h, aeval A x]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shatter.lean
@[simp] lemma mem_shatterer : s ∈ 𝒜.shatterer ↔ 𝒜.Shatters s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ ∃ a ∈ 𝒜, s ⊆ a

Tactic:
exact h.exists_superset

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
⊢ s ∈ 𝒜.shatterer ↔ 𝒜.Shatters s

Tactic:
refine mem_filter.trans <| and_iff_right_of_imp fun h ↦ ?_

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ s ∈ 𝒜.biUnion powerset

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ s ∈ 𝒜.biUnion powerset

Tactic:
simp_rw [mem_biUnion, mem_powerset]

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
h : 𝒜.Shatters s
⊢ ∃ a ∈ 𝒜, s ⊆ a
-- Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean
@[ext]
lemma FirstObj.ext (z₁ z₂ : FirstObj P R) (h : ∀ (Y : C) (f : Y ⟶ X)
    (hf : R f), (Pi.π _ ⟨Y, f, hf⟩ : FirstObj P R ⟶ _) z₁ =
      (Pi.π _ ⟨Y, f, hf⟩ : FirstObj P R ⟶ _) z₂) : z₁ = z₂

Proof state:
case w.mk.mk.mk
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
z₁ z₂ : FirstObj P R
h :
  ∀ (Y : C) (f : Y ⟶ X) (hf : R f),
    Pi.π (fun f => P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₁ = Pi.π (fun f => P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₂
Y : C
f : Y ⟶ X
hf : R f
⊢ limit.π (Discrete.functor fun f => P.obj (op f.fst)) { as := ⟨Y, ⟨f, hf⟩⟩ } z₁ =
    limit.π (Discrete.functor fun f => P.obj (op f.fst)) { as := ⟨Y, ⟨f, hf⟩⟩ } z₂

Tactic:
exact h Y f hf

Result:
no goals

Proof state:
case w
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
z₁ z₂ : FirstObj P R
h :
  ∀ (Y : C) (f : Y ⟶ X) (hf : R f),
    Pi.π (fun f => P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₁ = Pi.π (fun f => P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₂
⊢ ∀ (j : Discrete ((Y : C) × { f // R f })),
    limit.π (Discrete.functor fun f => P.obj (op f.fst)) j z₁ =
      limit.π (Discrete.functor fun f => P.obj (op f.fst)) j z₂

Tactic:
rintro ⟨⟨Y, f, hf⟩⟩

Result:
case w.mk.mk.mk
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
z₁ z₂ : FirstObj P R
h :
  ∀ (Y : C) (f : Y ⟶ X) (hf : R f),
    Pi.π (fun f => P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₁ = Pi.π (fun f => P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₂
Y : C
f : Y ⟶ X
hf : R f
⊢ limit.π (Discrete.functor fun f => P.obj (op f.fst)) { as := ⟨Y, ⟨f, hf⟩⟩ } z₁ =
    limit.π (Discrete.functor fun f => P.obj (op f.fst)) { as := ⟨Y, ⟨f, hf⟩⟩ } z₂

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
z₁ z₂ : FirstObj P R
h :
  ∀ (Y : C) (f : Y ⟶ X) (hf : R f),
    Pi.π (fun f => P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₁ = Pi.π (fun f => P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₂
⊢ z₁ = z₂

Tactic:
apply Limits.Types.limit_ext

Result:
case w
C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
z₁ z₂ : FirstObj P R
h :
  ∀ (Y : C) (f : Y ⟶ X) (hf : R f),
    Pi.π (fun f => P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₁ = Pi.π (fun f => P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩ z₂
⊢ ∀ (j : Discrete ((Y : C) × { f // R f })),
    limit.π (Discrete.functor fun f => P.obj (op f.fst)) j z₁ =
      limit.π (Discrete.functor fun f => P.obj (op f.fst)) j z₂
-- Mathlib/NumberTheory/DirichletCharacter/GaussSum.lean
/-- If `χ` is primitive, but `e` is not, then `gaussSum χ e = 0`. -/
lemma gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive [IsDomain R]
    {χ : DirichletCharacter R N} (hχ : IsPrimitive χ) (he : ¬IsPrimitive e) :
    gaussSum χ e = 0

Proof state:
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
he : ¬e.IsPrimitive
hχ : gaussSum χ e ≠ 0
⊢ ¬χ.IsPrimitive

Tactic:
rcases e.exists_divisor_of_not_isPrimitive he with ⟨d, hd₁, hd₂, hed⟩

Result:
case intro.intro.intro
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
he : ¬e.IsPrimitive
hχ : gaussSum χ e ≠ 0
d : ℕ
hd₁ : d ∣ N
hd₂ : d < N
hed : e.mulShift ↑d = 1
⊢ ¬χ.IsPrimitive

Proof state:
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
he : ¬e.IsPrimitive
⊢ gaussSum χ e = 0

Tactic:
contrapose! hχ

Result:
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
he : ¬e.IsPrimitive
hχ : gaussSum χ e ≠ 0
⊢ ¬χ.IsPrimitive

Proof state:
case intro.intro.intro
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
he : ¬e.IsPrimitive
hχ : gaussSum χ e ≠ 0
d : ℕ
hd₁ : d ∣ N
hd₂ : d < N
hed : e.mulShift ↑d = 1
this : χ.conductor ≤ d
⊢ ¬χ.IsPrimitive

Tactic:
exact (this.trans_lt hd₂).ne

Result:
no goals

Proof state:
case intro.intro.intro
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
he : ¬e.IsPrimitive
hχ : gaussSum χ e ≠ 0
d : ℕ
hd₁ : d ∣ N
hd₂ : d < N
hed : e.mulShift ↑d = 1
⊢ ¬χ.IsPrimitive

Tactic:
have : χ.conductor ≤ d := Nat.sInf_le <| factorsThrough_of_gaussSum_ne_zero e hd₁ hed hχ

Result:
case intro.intro.intro
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
he : ¬e.IsPrimitive
hχ : gaussSum χ e ≠ 0
d : ℕ
hd₁ : d ∣ N
hd₂ : d < N
hed : e.mulShift ↑d = 1
this : χ.conductor ≤ d
⊢ ¬χ.IsPrimitive
-- Mathlib/Topology/Algebra/Monoid.lean
theorem continuous_multiset_prod {f : ι → X → M} (s : Multiset ι) :
    (∀ i ∈ s, Continuous (f i)) → Continuous fun a => (s.map fun i => f i a).prod

Proof state:
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
⊢ (∀ i ∈ s, Continuous (f i)) → Continuous fun a => (Multiset.map (fun i => f i a) s).prod

Tactic:
rcases s with ⟨l⟩

Result:
case mk
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
l : List ι
⊢ (∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, Continuous (f i)) →
    Continuous fun a => (Multiset.map (fun i => f i a) (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Proof state:
case mk
ι : Type u_1
M : Type u_3
X : Type u_5
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace M
inst✝¹ : CommMonoid M
inst✝ : ContinuousMul M
f : ι → X → M
s : Multiset ι
l : List ι
⊢ (∀ i ∈ Quot.mk (⇑(List.isSetoid ι)) l, Continuous (f i)) →
    Continuous fun a => (Multiset.map (fun i => f i a) (Quot.mk (⇑(List.isSetoid ι)) l)).prod

Tactic:
simpa using continuous_list_prod l

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem fill_false {w : Nat} : fill w false = 0#w

Proof state:
w : Nat
⊢ fill w false = 0#w

Tactic:
simp [fill_eq]

Result:
no goals
-- Mathlib/Data/Nat/Find.lean
lemma findGreatest_mono_left [DecidablePred Q] (hPQ : ∀ n, P n → Q n) (n : ℕ) :
    Nat.findGreatest P n ≤ Nat.findGreatest Q n

Proof state:
case neg
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : ¬P (n + 1)
⊢ findGreatest P n ≤ findGreatest Q (n + 1)

Tactic:
exact le_trans hn (Nat.findGreatest_mono_right _ <| le_succ _)

Result:
no goals

Proof state:
case neg
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : ¬P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)

Tactic:
rw [findGreatest_of_not h]

Result:
case neg
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : ¬P (n + 1)
⊢ findGreatest P n ≤ findGreatest Q (n + 1)

Proof state:
case succ
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)

Tactic:
by_cases h : P (n + 1)

Result:
case pos
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)

case neg
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : ¬P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)

Proof state:
case zero
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
⊢ findGreatest P 0 ≤ findGreatest Q 0

Tactic:
rfl

Result:
no goals

Proof state:
case pos
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
n : ℕ
hn : findGreatest P n ≤ findGreatest Q n
h : P (n + 1)
⊢ findGreatest P (n + 1) ≤ findGreatest Q (n + 1)

Tactic:
rw [findGreatest_eq h, findGreatest_eq (hPQ _ h)]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basis.lean
lemma TensorProduct.sum_tmul_basis_right_eq_zero
    (b : κ →₀ M) (h : (b.sum fun i m ↦ m ⊗ₜ[R] 𝒞 i) = 0) : b = 0 :=
  have := Classical.decEq κ
  (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm.injective (a₂ := 0) <| by simpa

Proof state:
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
𝒞 : Basis κ R N
b : κ →₀ M
h : (b.sum fun i m => m ⊗ₜ[R] 𝒞 i) = 0
this : DecidableEq κ
⊢ (equivFinsuppOfBasisRight 𝒞).symm b = (equivFinsuppOfBasisRight 𝒞).symm 0

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem le_div_iff_mul_le (k0 : 0 < k) : x ≤ y / k ↔ x * k ≤ y

Proof state:
case ind.zero
y k : Nat
h : 0 < k ∧ k ≤ y
IH : ∀ {x : Nat}, 0 < k → (x ≤ (y - k) / k ↔ x * k ≤ y - k)
k0 : 0 < k
⊢ 0 ≤ (y - k) / k + 1 ↔ 0 * k ≤ y

Tactic:
simp [zero_le]

Result:
no goals

Proof state:
case base.succ
y k : Nat
h : ¬(0 < k ∧ k ≤ y)
k0 : 0 < k
x : Nat
⊢ y < k

Tactic:
exact Nat.not_le.1 fun h' => h ⟨k0, h'⟩

Result:
no goals

Proof state:
k x y : Nat
k0 : 0 < k
⊢ x ≤ y / k ↔ x * k ≤ y

Tactic:
induction y, k using mod.inductionOn generalizing x with
  (rw [div_eq]; simp [h]; cases x with | zero => simp [zero_le] | succ x => ?_)
| base y k h =>
  simp only [add_one, succ_mul, false_iff, Nat.not_le, Nat.succ_ne_zero]
  refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_left ..)
  exact Nat.not_le.1 fun h' => h ⟨k0, h'⟩
| ind y k h IH =>
  rw [Nat.add_le_add_iff_right, IH k0, succ_mul,
      ← Nat.add_sub_cancel (x*k) k, Nat.sub_le_sub_iff_right h.2, Nat.add_sub_cancel]

Result:
no goals

Proof state:
case ind
y k : Nat
h : 0 < k ∧ k ≤ y
IH : ∀ {x : Nat}, 0 < k → (x ≤ (y - k) / k ↔ x * k ≤ y - k)
x : Nat
k0 : 0 < k
⊢ x ≤ y / k ↔ x * k ≤ y

Tactic:
rw [div_eq]

Result:
case ind
y k : Nat
h : 0 < k ∧ k ≤ y
IH : ∀ {x : Nat}, 0 < k → (x ≤ (y - k) / k ↔ x * k ≤ y - k)
x : Nat
k0 : 0 < k
⊢ x ≤ ite (0 < k ∧ k ≤ y) ((y - k) / k + 1) 0 ↔ x * k ≤ y

Proof state:
case base.succ
y k : Nat
h : ¬(0 < k ∧ k ≤ y)
k0 : 0 < k
x : Nat
⊢ y < x * k + k

Tactic:
refine Nat.lt_of_lt_of_le ?_ (Nat.le_add_left ..)

Result:
case base.succ
y k : Nat
h : ¬(0 < k ∧ k ≤ y)
k0 : 0 < k
x : Nat
⊢ y < k

Proof state:
case ind
y k : Nat
h : 0 < k ∧ k ≤ y
IH : ∀ {x : Nat}, 0 < k → (x ≤ (y - k) / k ↔ x * k ≤ y - k)
x : Nat
k0 : 0 < k
⊢ x ≤ ite (0 < k ∧ k ≤ y) ((y - k) / k + 1) 0 ↔ x * k ≤ y

Tactic:
simp [h]

Result:
case ind
y k : Nat
h : 0 < k ∧ k ≤ y
IH : ∀ {x : Nat}, 0 < k → (x ≤ (y - k) / k ↔ x * k ≤ y - k)
x : Nat
k0 : 0 < k
⊢ x ≤ (y - k) / k + 1 ↔ x * k ≤ y

Proof state:
case ind
y k : Nat
h : 0 < k ∧ k ≤ y
IH : ∀ {x : Nat}, 0 < k → (x ≤ (y - k) / k ↔ x * k ≤ y - k)
x : Nat
k0 : 0 < k
⊢ x ≤ (y - k) / k + 1 ↔ x * k ≤ y

Tactic:
cases x with | zero => simp [zero_le] | succ x => ?_

Result:
case ind.succ
y k : Nat
h : 0 < k ∧ k ≤ y
IH : ∀ {x : Nat}, 0 < k → (x ≤ (y - k) / k ↔ x * k ≤ y - k)
k0 : 0 < k
x : Nat
⊢ x + 1 ≤ (y - k) / k + 1 ↔ (x + 1) * k ≤ y

Proof state:
case ind.succ
y k : Nat
h : 0 < k ∧ k ≤ y
IH : ∀ {x : Nat}, 0 < k → (x ≤ (y - k) / k ↔ x * k ≤ y - k)
k0 : 0 < k
x : Nat
⊢ x + 1 ≤ (y - k) / k + 1 ↔ (x + 1) * k ≤ y

Tactic:
rw [Nat.add_le_add_iff_right, IH k0, succ_mul,
    ← Nat.add_sub_cancel (x*k) k, Nat.sub_le_sub_iff_right h.2, Nat.add_sub_cancel]

Result:
no goals

Proof state:
case base.succ
y k : Nat
h : ¬(0 < k ∧ k ≤ y)
k0 : 0 < k
x : Nat
⊢ x + 1 = 0 ↔ (x + 1) * k ≤ y

Tactic:
simp only [add_one, succ_mul, false_iff, Nat.not_le, Nat.succ_ne_zero]

Result:
case base.succ
y k : Nat
h : ¬(0 < k ∧ k ≤ y)
k0 : 0 < k
x : Nat
⊢ y < x * k + k
-- Mathlib/LinearAlgebra/Prod.lean
theorem inr_injective : Function.Injective (inr R M M₂) := fun _ => by simp

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M₂
⊢ ∀ ⦃a₂ : M₂⦄, (inr R M M₂) x✝ = (inr R M M₂) a₂ → x✝ = a₂

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/Impartial.lean
theorem exists_right_move_equiv_iff_fuzzy_zero : (∃ j, G.moveRight j ≈ 0) ↔ G ‖ 0

Proof state:
G : PGame
inst✝ : G.Impartial
hn : ∃ j, G.moveRight j ≤ 0
⊢ ∃ j, G.moveRight j ≈ 0

Tactic:
obtain ⟨i, hi⟩ := hn

Result:
case intro
G : PGame
inst✝ : G.Impartial
i : G.RightMoves
hi : G.moveRight i ≤ 0
⊢ ∃ j, G.moveRight j ≈ 0

Proof state:
case intro
G : PGame
inst✝ : G.Impartial
i : G.RightMoves
hi : G.moveRight i ≤ 0
⊢ ∃ j, G.moveRight j ≈ 0

Tactic:
exact ⟨i, (equiv_zero_iff_le _).2 hi⟩

Result:
no goals

Proof state:
G : PGame
inst✝ : G.Impartial
hn : G ‖ 0
⊢ ∃ j, G.moveRight j ≈ 0

Tactic:
rw [fuzzy_zero_iff_lf G, lf_zero_le] at hn

Result:
G : PGame
inst✝ : G.Impartial
hn : ∃ j, G.moveRight j ≤ 0
⊢ ∃ j, G.moveRight j ≈ 0

Proof state:
G : PGame
inst✝ : G.Impartial
⊢ (∃ j, G.moveRight j ≈ 0) ↔ G ‖ 0

Tactic:
refine ⟨fun ⟨i, hi⟩ => (fuzzy_zero_iff_lf G).2 (lf_of_moveRight_le hi.1), fun hn => ?_⟩

Result:
G : PGame
inst✝ : G.Impartial
hn : G ‖ 0
⊢ ∃ j, G.moveRight j ≈ 0
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem toLinearPMap_graph_eq (g : Submodule R (E × F))
    (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) :
    g.toLinearPMap.graph = g

Proof state:
case h.mk.mpr
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
hx_fst : x_fst ∈ map (LinearMap.fst R E F) g
⊢ ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑g.toLinearPMap y = (x_fst, x_snd).2

Tactic:
refine ⟨⟨x_fst, hx_fst⟩, Subtype.coe_mk x_fst hx_fst, ?_⟩

Result:
case h.mk.mpr
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
hx : (x_fst, x_snd) ∈ g
hx_fst : x_fst ∈ map (LinearMap.fst R E F) g
⊢ ↑g.toLinearPMap ⟨x_fst, hx_fst⟩ = (x_fst, x_snd).2

Proof state:
case h.mk.mp
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
hx : ∃ y, ↑y = (x_fst, x_snd).1 ∧ ↑g.toLinearPMap y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ g

Tactic:
rcases hx with ⟨y, hx1, hx2⟩

Result:
case h.mk.mp.intro.intro
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
x_fst : E
x_snd : F
y : ↥g.toLinearPMap.domain
hx1 : ↑y = (x_fst, x_snd).1
hx2 : ↑g.toLinearPMap y = (x_fst, x_snd).2
⊢ (x_fst, x_snd) ∈ g