harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem exists_mem_push {p : α → Prop} {a : α} {xs : Vector α n} :
    (∃ x, ∃ _ : x ∈ xs.push a, p x) ↔ p a ∨ ∃ x, ∃ _ : x ∈ xs, p x

Proof state:
α : Type u_1
n : Nat
p : α → Prop
a : α
xs : Vector α n
⊢ (∃ x x_1, p x) ↔ p a ∨ ∃ x x_1, p x

Tactic:
simp only [mem_push, exists_prop]

Result:
α : Type u_1
n : Nat
p : α → Prop
a : α
xs : Vector α n
⊢ (∃ x, (x ∈ xs ∨ x = a) ∧ p x) ↔ p a ∨ ∃ x, x ∈ xs ∧ p x

Proof state:
case mp
α : Type u_1
n : Nat
p : α → Prop
a : α
xs : Vector α n
⊢ (∃ x, (x ∈ xs ∨ x = a) ∧ p x) → p a ∨ ∃ x, x ∈ xs ∧ p x

Tactic:
rintro ⟨x, (h | rfl), h'⟩

Result:
case mp.intro.intro.inl
α : Type u_1
n : Nat
p : α → Prop
a : α
xs : Vector α n
x : α
h' : p x
h : x ∈ xs
⊢ p a ∨ ∃ x, x ∈ xs ∧ p x

case mp.intro.intro.inr
α : Type u_1
n : Nat
p : α → Prop
xs : Vector α n
x : α
h' : p x
⊢ p x ∨ ∃ x, x ∈ xs ∧ p x

Proof state:
α : Type u_1
n : Nat
p : α → Prop
a : α
xs : Vector α n
h : p a
⊢ a ∈ xs ∨ a = a

Tactic:
simp

Result:
no goals

Proof state:
case mp.intro.intro.inr
α : Type u_1
n : Nat
p : α → Prop
xs : Vector α n
x : α
h' : p x
⊢ p x ∨ ∃ x, x ∈ xs ∧ p x

Tactic:
exact .inl h'

Result:
no goals

Proof state:
case mpr
α : Type u_1
n : Nat
p : α → Prop
a : α
xs : Vector α n
⊢ (p a ∨ ∃ x, x ∈ xs ∧ p x) → ∃ x, (x ∈ xs ∨ x = a) ∧ p x

Tactic:
rintro (h | ⟨x, h, h'⟩)

Result:
case mpr.inl
α : Type u_1
n : Nat
p : α → Prop
a : α
xs : Vector α n
h : p a
⊢ ∃ x, (x ∈ xs ∨ x = a) ∧ p x

case mpr.inr.intro.intro
α : Type u_1
n : Nat
p : α → Prop
a : α
xs : Vector α n
x : α
h : x ∈ xs
h' : p x
⊢ ∃ x, (x ∈ xs ∨ x = a) ∧ p x

Proof state:
case mpr.inl
α : Type u_1
n : Nat
p : α → Prop
a : α
xs : Vector α n
h : p a
⊢ ∃ x, (x ∈ xs ∨ x = a) ∧ p x

Tactic:
exact ⟨a, by simp, h⟩

Result:
no goals

Proof state:
α : Type u_1
n : Nat
p : α → Prop
a : α
xs : Vector α n
⊢ (∃ x, (x ∈ xs ∨ x = a) ∧ p x) ↔ p a ∨ ∃ x, x ∈ xs ∧ p x

Tactic:
constructor

Result:
case mp
α : Type u_1
n : Nat
p : α → Prop
a : α
xs : Vector α n
⊢ (∃ x, (x ∈ xs ∨ x = a) ∧ p x) → p a ∨ ∃ x, x ∈ xs ∧ p x

case mpr
α : Type u_1
n : Nat
p : α → Prop
a : α
xs : Vector α n
⊢ (p a ∨ ∃ x, x ∈ xs ∧ p x) → ∃ x, (x ∈ xs ∨ x = a) ∧ p x

Proof state:
case mp.intro.intro.inl
α : Type u_1
n : Nat
p : α → Prop
a : α
xs : Vector α n
x : α
h' : p x
h : x ∈ xs
⊢ p a ∨ ∃ x, x ∈ xs ∧ p x

Tactic:
exact .inr ⟨x, h, h'⟩

Result:
no goals

Proof state:
case mpr.inr.intro.intro
α : Type u_1
n : Nat
p : α → Prop
a : α
xs : Vector α n
x : α
h : x ∈ xs
h' : p x
⊢ ∃ x, (x ∈ xs ∨ x = a) ∧ p x

Tactic:
exact ⟨x, .inl h, h'⟩

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem compl_cylinder (s : Finset ι) (S : Set (∀ i : s, α i)) :
    (cylinder s S)ᶜ = cylinder s (Sᶜ)

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
⊢ (cylinder s S)ᶜ = cylinder s Sᶜ

Tactic:
ext1 f

Result:
case h
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
f : (i : ι) → α i
⊢ f ∈ (cylinder s S)ᶜ ↔ f ∈ cylinder s Sᶜ

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S : Set ((i : { x // x ∈ s }) → α ↑i)
f : (i : ι) → α i
⊢ f ∈ (cylinder s S)ᶜ ↔ f ∈ cylinder s Sᶜ

Tactic:
simp only [mem_compl_iff, mem_cylinder]

Result:
no goals
-- Mathlib/Computability/RegularExpressions.lean
theorem star_rmatch_iff (P : RegularExpression α) :
    ∀ x : List α, (star P).rmatch x ↔ ∃ S : List (List α), x
          = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t :=
  fun x => by
    have IH := fun t (_h : List.length t < List.length x) => star_rmatch_iff P t
    clear star_rmatch_iff
    constructor
    · rcases x with - | ⟨a, x⟩
      · intro _h
        use []; dsimp; tauto
      · rw [rmatch, deriv, mul_rmatch_iff]
        rintro ⟨t, u, hs, ht, hu⟩
        have hwf : u.length < (List.cons a x).length

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
⊢ a :: x = ((a :: t) :: S').flatten ∧ ∀ t_1 ∈ (a :: t) :: S', t_1 ≠ [] ∧ P.rmatch t_1 = true

Tactic:
constructor

Result:
case h.left
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
⊢ a :: x = ((a :: t) :: S').flatten

case h.right
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
t u : List α
hs : x = t ++ u
ht : (P.deriv a).rmatch t = true
hwf : u.length < (a :: x).length
S' : List (List α)
hsum : u = S'.flatten
helem : ∀ t ∈ S', t ≠ [] ∧ P.rmatch t = true
⊢ ∀ t_1 ∈ (a :: t) :: S', t_1 ≠ [] ∧ P.rmatch t_1 = true

Proof state:
case mpr.intro.intro.cons.cons.cons.refine_2
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
U : List (List α)
b : α
t✝ : List α
helem : ∀ t ∈ (b :: t✝) :: U, t ≠ [] ∧ P.rmatch t = true
hsum : a = b ∧ x = t✝ ++ U.flatten
hwf : U.flatten.length < (a :: x).length
t : List α
h : t ∈ U
⊢ t ∈ (b :: t✝) :: U

Tactic:
right

Result:
case mpr.intro.intro.cons.cons.cons.refine_2.a
α : Type u_1
inst✝ : DecidableEq α
P : RegularExpression α
a : α
x : List α
IH :
  ∀ (t : List α),
    t.length < (a :: x).length → (P.star.rmatch t = true ↔ ∃ S, t = S.flatten ∧ ∀ t ∈ S, t ≠ [] ∧ P.rmatch t = true)
U : List (List α)
b : α
t✝ : List α
helem : ∀ t ∈ (b :: t✝) :: U, t ≠ [] ∧ P.rmatch t = true
hsum : a = b ∧ x = t✝ ++ U.flatten
hwf : U.flatten.length < (a :: x).length
t : List α
h : t ∈ U
⊢ Mem t U
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem algebraMap_mk {A : Type*} [Semiring A] [Algebra R A] (a : R) (s : S) :
    algebraMap _ _ (Localization.mk a s) = mk (algebraMap R A a) s

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ (algebraMap (Localization S) (LocalizedModule S A)) (IsLocalization.mk' (Localization S) a s) =
    mk ((algebraMap R A) a) s

Tactic:
exact algebraMap_mk' ..

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ (algebraMap (Localization S) (LocalizedModule S A)) (Localization.mk a s) = mk ((algebraMap R A) a) s

Tactic:
rw [Localization.mk_eq_mk']

Result:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
a : R
s : ↥S
⊢ (algebraMap (Localization S) (LocalizedModule S A)) (IsLocalization.mk' (Localization S) a s) =
    mk ((algebraMap R A) a) s
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem map_add_supp (a : R) {s : R} (h : s ∈ supp v) : v (a + s) = v a

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
⊢ v (a + s) = v a

Tactic:
have aux : ∀ a s, v s = 0 → v (a + s) ≤ v a := by
  intro a' s' h'
  refine le_trans (v.map_add a' s') (max_le le_rfl ?_)
  simp [h']

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
aux : ∀ (a s : R), v s = 0 → v (a + s) ≤ v a
⊢ v (a + s) = v a

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
aux : ∀ (a s : R), v s = 0 → v (a + s) ≤ v a
⊢ v (a + s) = v a

Tactic:
apply le_antisymm (aux a s h)

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
aux : ∀ (a s : R), v s = 0 → v (a + s) ≤ v a
⊢ v a ≤ v (a + s)

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
⊢ ∀ (a s : R), v s = 0 → v (a + s) ≤ v a

Tactic:
intro a' s' h'

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
a' s' : R
h' : v s' = 0
⊢ v (a' + s') ≤ v a'

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
a' s' : R
h' : v s' = 0
⊢ v (a' + s') ≤ v a'

Tactic:
refine le_trans (v.map_add a' s') (max_le le_rfl ?_)

Result:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
a' s' : R
h' : v s' = 0
⊢ v s' ≤ v a'

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
aux : ∀ (a s : R), v s = 0 → v (a + s) ≤ v a
⊢ v (-s) = 0

Tactic:
rwa [← Ideal.neg_mem_iff] at h

Result:
no goals

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
a' s' : R
h' : v s' = 0
⊢ v s' ≤ v a'

Tactic:
simp [h']

Result:
no goals

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
aux : ∀ (a s : R), v s = 0 → v (a + s) ≤ v a
⊢ v a ≤ v (a + s)

Tactic:
calc
  v a = v (a + s + -s) := by simp
  _ ≤ v (a + s) := aux (a + s) (-s) (by rwa [← Ideal.neg_mem_iff] at h)

Result:
no goals

Proof state:
R : Type u_3
Γ₀ : Type u_4
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
a s : R
h : s ∈ v.supp
aux : ∀ (a s : R), v s = 0 → v (a + s) ≤ v a
⊢ v a = v (a + s + -s)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean
theorem exists_isTranscendenceBasis' (R : Type u) {A : Type v} [CommRing R] [CommRing A]
    [Algebra R A] (h : Injective (algebraMap R A)) :
    ∃ (ι : Type v) (x : ι → A), IsTranscendenceBasis R x

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Injective ⇑(algebraMap R A)
⊢ ∃ ι x, IsTranscendenceBasis R x

Tactic:
obtain ⟨s, h⟩ := exists_isTranscendenceBasis R h

Result:
case intro
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h✝ : Injective ⇑(algebraMap R A)
s : Set A
h : IsTranscendenceBasis R Subtype.val
⊢ ∃ ι x, IsTranscendenceBasis R x

Proof state:
case intro
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h✝ : Injective ⇑(algebraMap R A)
s : Set A
h : IsTranscendenceBasis R Subtype.val
⊢ ∃ ι x, IsTranscendenceBasis R x

Tactic:
exact ⟨s, Subtype.val, h⟩

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Summable.lean
theorem pow_finite_co_support {x : HahnSeries Γ R} (hx : 0 < x.orderTop) (g : Γ) :
    Set.Finite {a | ((fun n ↦ x ^ n) a).coeff g ≠ 0}

Proof state:
case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
⊢ {a | ((fun n => x ^ n) a).coeff g ≠ 0}.Finite

case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∉ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
⊢ {a | ((fun n => x ^ n) a).coeff g ≠ 0}.Finite

Tactic:
swap

Result:
case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∉ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
⊢ {a | ((fun n => x ^ n) a).coeff g ≠ 0}.Finite

case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
hg : g ∈ ⋃ n, {g | (x ^ n).coeff g ≠ 0}
⊢ {a | ((fun n => x ^ n) a).coeff g ≠ 0}.Finite

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
⊢ {a | ((fun n => x ^ n) a).coeff g ≠ 0}.Finite

Tactic:
by_cases h0 : x = 0

Result:
case pos
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : x = 0
⊢ {a | ((fun n => x ^ n) a).coeff g ≠ 0}.Finite

case neg
Γ : Type u_1
R : Type u_3
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : CommRing R
x : HahnSeries Γ R
hx : 0 < x.orderTop
g : Γ
hpwo : (⋃ n, (x ^ n).support).IsPWO
h0 : ¬x = 0
⊢ {a | ((fun n => x ^ n) a).coeff g ≠ 0}.Finite
-- Mathlib/FieldTheory/Finite/Trace.lean
theorem trace_to_zmod_nondegenerate (F : Type*) [Field F] [Finite F]
    [Algebra (ZMod (ringChar F)) F] {a : F} (ha : a ≠ 0) :
    ∃ b : F, Algebra.trace (ZMod (ringChar F)) F (a * b) ≠ 0

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
⊢ ∃ b, (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0

Tactic:
haveI : Fact (ringChar F).Prime := ⟨CharP.char_is_prime F _⟩

Result:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
⊢ ∃ b, (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
htr : (∀ (n : F), ((Algebra.traceForm (ZMod (ringChar F)) F) a) n = 0) → a = 0
⊢ ∃ b, (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0

Tactic:
simp_rw [Algebra.traceForm_apply] at htr

Result:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
htr : (∀ (n : F), (Algebra.trace (ZMod (ringChar F)) F) (a * n) = 0) → a = 0
⊢ ∃ b, (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
htr : (∀ (n : F), (Algebra.trace (ZMod (ringChar F)) F) (a * n) = 0) → a = 0
⊢ ∃ b, (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0

Tactic:
by_contra! hf

Result:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
htr : (∀ (n : F), (Algebra.trace (ZMod (ringChar F)) F) (a * n) = 0) → a = 0
hf : ∀ (b : F), (Algebra.trace (ZMod (ringChar F)) F) (a * b) = 0
⊢ False

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
htr : (∀ (n : F), (Algebra.trace (ZMod (ringChar F)) F) (a * n) = 0) → a = 0
hf : ∀ (b : F), (Algebra.trace (ZMod (ringChar F)) F) (a * b) = 0
⊢ False

Tactic:
exact ha (htr hf)

Result:
no goals

Proof state:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
⊢ ∃ b, (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0

Tactic:
have htr := traceForm_nondegenerate (ZMod (ringChar F)) F a

Result:
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
htr : (∀ (n : F), ((Algebra.traceForm (ZMod (ringChar F)) F) a) n = 0) → a = 0
⊢ ∃ b, (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval_comp : (p.comp q).eval x = p.eval (q.eval x)

Proof state:
case h_add
R : Type u
inst✝ : CommSemiring R
p q : R[X]
x : R
r s : R[X]
hr : eval x (r.comp q) = eval (eval x q) r
hs : eval x (s.comp q) = eval (eval x q) s
⊢ eval x ((r + s).comp q) = eval (eval x q) (r + s)

Tactic:
simp [add_comp, hr, hs]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
x : R
⊢ eval x (p.comp q) = eval (eval x q) p

Tactic:
induction p using Polynomial.induction_on' with
| h_add r s hr hs =>
  simp [add_comp, hr, hs]
| h_monomial n a =>
  simp

Result:
no goals

Proof state:
case h_monomial
R : Type u
inst✝ : CommSemiring R
p q : R[X]
x : R
n : ℕ
a : R
⊢ eval x (((monomial n) a).comp q) = eval (eval x q) ((monomial n) a)

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem DenseRange.topologicalClosure_map_subgroup [Group H] [TopologicalSpace H]
    [IsTopologicalGroup H] {f : G →* H} (hf : Continuous f) (hf' : DenseRange f) {s : Subgroup G}
    (hs : s.topologicalClosure = ⊤) : (s.map f).topologicalClosure = ⊤

Proof state:
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous ⇑f
hf' : DenseRange ⇑f
s : Subgroup G
hs : Dense ↑s
⊢ Dense ↑(Subgroup.map f s)

Tactic:
exact hf'.dense_image hf hs

Result:
no goals

Proof state:
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous ⇑f
hf' : DenseRange ⇑f
s : Subgroup G
hs : ↑s.topologicalClosure = ↑⊤
⊢ ↑(Subgroup.map f s).topologicalClosure = ↑⊤

Tactic:
simp only [Subgroup.topologicalClosure_coe, Subgroup.coe_top, ← dense_iff_closure_eq] at hs ⊢

Result:
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous ⇑f
hf' : DenseRange ⇑f
s : Subgroup G
hs : Dense ↑s
⊢ Dense ↑(Subgroup.map f s)

Proof state:
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous ⇑f
hf' : DenseRange ⇑f
s : Subgroup G
hs : s.topologicalClosure = ⊤
⊢ (Subgroup.map f s).topologicalClosure = ⊤

Tactic:
rw [SetLike.ext'_iff] at hs ⊢

Result:
G : Type w
H : Type x
inst✝⁵ : TopologicalSpace G
inst✝⁴ : Group G
inst✝³ : IsTopologicalGroup G
inst✝² : Group H
inst✝¹ : TopologicalSpace H
inst✝ : IsTopologicalGroup H
f : G →* H
hf : Continuous ⇑f
hf' : DenseRange ⇑f
s : Subgroup G
hs : ↑s.topologicalClosure = ↑⊤
⊢ ↑(Subgroup.map f s).topologicalClosure = ↑⊤
-- Mathlib/Tactic/Linarith/Lemmas.lean
theorem lt_of_eq_of_lt {α} [OrderedSemiring α] {a b : α} (ha : a = 0) (hb : b < 0) : a + b < 0

Proof state:
α : Type u_1
inst✝ : OrderedSemiring α
a b : α
ha : a = 0
hb : b < 0
⊢ a + b < 0

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean
protected lemma GrowsPolynomially.zpow (p : ℤ) (hf : GrowsPolynomially f)
    (hf_nonneg : ∀ᶠ x in atTop, 0 ≤ f x) : GrowsPolynomially fun x => (f x) ^ p

Proof state:
f : ℝ → ℝ
p : ℤ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x => f x ^ ↑p

Tactic:
exact hf.rpow p hf_nonneg

Result:
no goals

Proof state:
f : ℝ → ℝ
p : ℤ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x => f x ^ p

Tactic:
simp_rw [← rpow_intCast]

Result:
f : ℝ → ℝ
p : ℤ
hf : GrowsPolynomially f
hf_nonneg : ∀ᶠ (x : ℝ) in atTop, 0 ≤ f x
⊢ GrowsPolynomially fun x => f x ^ ↑p
-- Mathlib/Order/Filter/Prod.lean
theorem prod_principal_principal {s : Set α} {t : Set β} : 𝓟 s ×ˢ 𝓟 t = 𝓟 (s ×ˢ t)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ 𝓟 s ×ˢ 𝓟 t = 𝓟 (s ×ˢ t)

Tactic:
simp only [prod_eq_inf, comap_principal, principal_eq_iff_eq, comap_principal, inf_principal]

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t = s ×ˢ t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ Prod.fst ⁻¹' s ∩ Prod.snd ⁻¹' t = s ×ˢ t

Tactic:
rfl

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
theorem IndepSets.union {s₁ s₂ s' : Set (Set Ω)} {_mΩ : MeasurableSpace Ω}
    {κ : Kernel α Ω} {μ : Measure α}
    (h₁ : IndepSets s₁ s' κ μ) (h₂ : IndepSets s₂ s' κ μ) :
    IndepSets (s₁ ∪ s₂) s' κ μ

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s₁ s₂ s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h₁ : IndepSets s₁ s' κ μ
h₂ : IndepSets s₂ s' κ μ
⊢ IndepSets (s₁ ∪ s₂) s' κ μ

Tactic:
intro t1 t2 ht1 ht2

Result:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s₁ s₂ s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h₁ : IndepSets s₁ s' κ μ
h₂ : IndepSets s₂ s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₁ ∪ s₂
ht2 : t2 ∈ s'
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s₁ s₂ s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h₁ : IndepSets s₁ s' κ μ
h₂ : IndepSets s₂ s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₁ ∪ s₂
ht2 : t2 ∈ s'
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
rcases (Set.mem_union _ _ _).mp ht1 with ht1₁ | ht1₂

Result:
case inl
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s₁ s₂ s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h₁ : IndepSets s₁ s' κ μ
h₂ : IndepSets s₂ s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₁ ∪ s₂
ht2 : t2 ∈ s'
ht1₁ : t1 ∈ s₁
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

case inr
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s₁ s₂ s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h₁ : IndepSets s₁ s' κ μ
h₂ : IndepSets s₂ s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₁ ∪ s₂
ht2 : t2 ∈ s'
ht1₂ : t1 ∈ s₂
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Proof state:
case inl
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s₁ s₂ s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h₁ : IndepSets s₁ s' κ μ
h₂ : IndepSets s₂ s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₁ ∪ s₂
ht2 : t2 ∈ s'
ht1₁ : t1 ∈ s₁
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
exact h₁ t1 t2 ht1₁ ht2

Result:
no goals

Proof state:
case inr
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s₁ s₂ s' : Set (Set Ω)
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h₁ : IndepSets s₁ s' κ μ
h₂ : IndepSets s₂ s' κ μ
t1 t2 : Set Ω
ht1 : t1 ∈ s₁ ∪ s₂
ht2 : t2 ∈ s'
ht1₂ : t1 ∈ s₂
⊢ ∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2

Tactic:
exact h₂ t1 t2 ht1₂ ht2

Result:
no goals