harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
/-- Pull-out property of the conditional expectation. -/
lemma condExp_mul_of_aestronglyMeasurable_right {f g : α → ℝ} (hg : AEStronglyMeasurable[m] g μ)
    (hfg : Integrable (f * g) μ) (hf : Integrable f μ) : μ[f * g | m] =ᵐ[μ] μ[f | m] * g

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hg : AEStronglyMeasurable g μ
hfg : Integrable (f * g) μ
hf : Integrable f μ
⊢ μ[f * g|m] =ᶠ[ae μ] μ[f|m] * g

Tactic:
simpa [mul_comm] using condExp_mul_of_aestronglyMeasurable_left hg (mul_comm f g ▸ hfg) hf

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
lemma IsBase.map {B : Set α} (hB : M.IsBase B) {f : α → β} (hf) : (M.map f hf).IsBase (f '' B)

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α → β
hf : InjOn f M.E
⊢ (M.map f hf).IsBase (f '' B)

Tactic:
rw [map_isBase_iff]

Result:
α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α → β
hf : InjOn f M.E
⊢ ∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
B : Set α
hB : M.IsBase B
f : α → β
hf : InjOn f M.E
⊢ ∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀

Tactic:
exact ⟨B, hB, rfl⟩

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem map_comp (p q : R[X]) : map f (p.comp q) = (map f p).comp (map f q) :=
  Polynomial.induction_on p (by simp only [map_C, forall_const, C_comp, eq_self_iff_true])
    (by
      simp +contextual only [Polynomial.map_add, add_comp, forall_const,
        imp_true_iff, eq_self_iff_true])
    (by
      simp +contextual only [pow_succ, ← mul_assoc, comp, forall_const,
        eval₂_mul_X, imp_true_iff, eq_self_iff_true, map_X, Polynomial.map_mul])

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p q : R[X]
⊢ ∀ (a : R), map f ((C a).comp q) = (map f (C a)).comp (map f q)

Tactic:
simp only [map_C, forall_const, C_comp, eq_self_iff_true]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p q : R[X]
⊢ ∀ (p q_1 : R[X]),
    map f (p.comp q) = (map f p).comp (map f q) →
      map f (q_1.comp q) = (map f q_1).comp (map f q) → map f ((p + q_1).comp q) = (map f (p + q_1)).comp (map f q)

Tactic:
simp +contextual only [Polynomial.map_add, add_comp, forall_const,
  imp_true_iff, eq_self_iff_true]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p q : R[X]
⊢ ∀ (n : ℕ) (a : R),
    map f ((C a * X ^ n).comp q) = (map f (C a * X ^ n)).comp (map f q) →
      map f ((C a * X ^ (n + 1)).comp q) = (map f (C a * X ^ (n + 1))).comp (map f q)

Tactic:
simp +contextual only [pow_succ, ← mul_assoc, comp, forall_const,
  eval₂_mul_X, imp_true_iff, eq_self_iff_true, map_X, Polynomial.map_mul]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem le_natDegree_of_ne_zero (h : coeff p n ≠ 0) : n ≤ natDegree p

Proof state:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ p ≠ 0

Tactic:
rintro rfl

Result:
R : Type u
n : ℕ
inst✝ : Semiring R
h : coeff 0 n ≠ 0
⊢ False

Proof state:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ n ≤ p.natDegree

Tactic:
rw [← Nat.cast_le (α := WithBot ℕ), ← degree_eq_natDegree]

Result:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ ↑n ≤ p.degree

R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ p ≠ 0

Proof state:
R : Type u
n : ℕ
inst✝ : Semiring R
h : coeff 0 n ≠ 0
⊢ False

Tactic:
exact h rfl

Result:
no goals

Proof state:
R : Type u
n : ℕ
inst✝ : Semiring R
p : R[X]
h : p.coeff n ≠ 0
⊢ ↑n ≤ p.degree

Tactic:
exact le_degree_of_ne_zero h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem Bool.not_beq_not : ∀ (a b : Bool), ((!a) == (!b)) = (a == b)

Proof state:
⊢ ∀ (a b : Bool), ((!a) == !b) = (a == b)

Tactic:
decide

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem adjoin_simple_le_iff {K : IntermediateField F E} : F⟮α⟯ ≤ K ↔ α ∈ K

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
K : IntermediateField F E
⊢ F⟮α⟯ ≤ K ↔ α ∈ K

Tactic:
simp

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem minimalPeriod_eq_minimalPeriod_iff {g : β → β} {y : β} :
    minimalPeriod f x = minimalPeriod g y ↔ ∀ n, IsPeriodicPt f n x ↔ IsPeriodicPt g n y

Proof state:
α : Type u_1
β : Type u_2
f : α → α
x : α
g : β → β
y : β
⊢ minimalPeriod f x = minimalPeriod g y ↔ ∀ (n : ℕ), IsPeriodicPt f n x ↔ IsPeriodicPt g n y

Tactic:
simp_rw [isPeriodicPt_iff_minimalPeriod_dvd, dvd_right_iff_eq]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem thickening_eq_biUnion_ball {δ : ℝ} {E : Set X} : thickening δ E = ⋃ x ∈ E, ball x δ

Proof state:
case h
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
x : X
⊢ x ∈ thickening δ E ↔ x ∈ ⋃ x ∈ E, ball x δ

Tactic:
simp only [mem_iUnion₂, exists_prop]

Result:
case h
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
x : X
⊢ x ∈ thickening δ E ↔ ∃ i ∈ E, x ∈ ball i δ

Proof state:
case h
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
x : X
⊢ x ∈ thickening δ E ↔ ∃ i ∈ E, x ∈ ball i δ

Tactic:
exact mem_thickening_iff

Result:
no goals

Proof state:
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
⊢ thickening δ E = ⋃ x ∈ E, ball x δ

Tactic:
ext x

Result:
case h
X : Type u
inst✝ : PseudoMetricSpace X
δ : ℝ
E : Set X
x : X
⊢ x ∈ thickening δ E ↔ x ∈ ⋃ x ∈ E, ball x δ
-- Mathlib/Data/Finset/Sum.lean
@[simp] lemma mem_toLeft {x : α} : x ∈ u.toLeft ↔ inl x ∈ u

Proof state:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
x : α
⊢ x ∈ u.toLeft ↔ inl x ∈ u

Tactic:
simp [toLeft]

Result:
no goals
-- Mathlib/Order/Filter/Lift.lean
theorem map_lift'_eq {m : β → γ} (hh : Monotone h) : map m (f.lift' h) = f.lift' (image m ∘ h) :=
  calc
    map m (f.lift' h) = f.lift (map m ∘ 𝓟 ∘ h) := map_lift_eq <| monotone_principal.comp hh
    _ = f.lift' (image m ∘ h)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : Filter α
h : Set α → Set β
m : β → γ
hh : Monotone h
⊢ f.lift (map m ∘ 𝓟 ∘ h) = f.lift' (image m ∘ h)

Tactic:
simp only [comp_def, Filter.lift', map_principal]

Result:
no goals
-- Mathlib/Data/List/Infix.lean
theorem length_inits (l : List α) : length (inits l) = length l + 1

Proof state:
α : Type u_1
l : List α
⊢ l.inits.length = l.length + 1

Tactic:
simp [inits_eq_tails]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem Commute.zpow_right {A B : M} (h : Commute A B) (m : ℤ) : Commute A (B ^ m)

Proof state:
case inr.ofNat
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
hB : B⁻¹ = 0
a✝ : ℕ
⊢ Commute A (B ^ ofNat a✝)

Tactic:
simpa using h.pow_right _

Result:
no goals

Proof state:
case inl.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
hB : B⁻¹ * B = 1
right✝ : B * B⁻¹ = 1
⊢ Commute A (B ^ m)

Tactic:
refine SemiconjBy.zpow_right ?_ ?_ h _ <;> exact isUnit_det_of_left_inverse hB

Result:
no goals

Proof state:
case inr.negSucc
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
hB : B⁻¹ = 0
a✝ : ℕ
⊢ Commute A (B ^ -[a✝+1])

Tactic:
simp [← inv_pow', hB]

Result:
no goals

Proof state:
case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
hB : B⁻¹ = 0
⊢ Commute A (B ^ m)

Tactic:
cases m

Result:
case inr.ofNat
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
hB : B⁻¹ = 0
a✝ : ℕ
⊢ Commute A (B ^ ofNat a✝)

case inr.negSucc
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
hB : B⁻¹ = 0
a✝ : ℕ
⊢ Commute A (B ^ -[a✝+1])

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
⊢ Commute A (B ^ m)

Tactic:
rcases nonsing_inv_cancel_or_zero B with (⟨hB, _⟩ | hB)

Result:
case inl.intro
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
hB : B⁻¹ * B = 1
right✝ : B * B⁻¹ = 1
⊢ Commute A (B ^ m)

case inr
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A B : M
h : Commute A B
m : ℤ
hB : B⁻¹ = 0
⊢ Commute A (B ^ m)
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBase.exchange_isBase_of_indep' (hB : M.IsBase B) (he : e ∈ B) (hf : f ∉ B)
    (hI : M.Indep (insert f B \ {e})) : M.IsBase (insert f B \ {e})

Proof state:
α : Type u_1
M : Matroid α
B : Set α
f : α
hB : M.IsBase B
hf : f ∉ B
he : f ∈ B
hI : M.Indep (insert f B \ {f})
⊢ False

Tactic:
exact hf he

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
hfe : f ≠ e
⊢ M.IsBase (insert f (B \ {e}))

Tactic:
exact hB.exchange_isBase_of_indep hf hI

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ B
hI : M.Indep (insert f B \ {e})
hfe : f ≠ e
⊢ M.IsBase (insert f B \ {e})

Tactic:
rw [← insert_diff_singleton_comm hfe] at *

Result:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ B
hI : M.Indep (insert f (B \ {e}))
hfe : f ≠ e
⊢ M.IsBase (insert f (B \ {e}))

Proof state:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ B
hI : M.Indep (insert f B \ {e})
⊢ f ≠ e

Tactic:
rintro rfl

Result:
α : Type u_1
M : Matroid α
B : Set α
f : α
hB : M.IsBase B
hf : f ∉ B
he : f ∈ B
hI : M.Indep (insert f B \ {f})
⊢ False

Proof state:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ B
hI : M.Indep (insert f B \ {e})
⊢ M.IsBase (insert f B \ {e})

Tactic:
have hfe : f ≠ e := by rintro rfl; exact hf he

Result:
α : Type u_1
M : Matroid α
B : Set α
e f : α
hB : M.IsBase B
he : e ∈ B
hf : f ∉ B
hI : M.Indep (insert f B \ {e})
hfe : f ≠ e
⊢ M.IsBase (insert f B \ {e})
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem aroots_pow [CommRing S] [IsDomain S] [Algebra T S] (p : T[X]) (n : ℕ) :
    (p ^ n).aroots S = n • p.aroots S

Proof state:
S : Type v
T : Type w
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
p : T[X]
n : ℕ
⊢ (p ^ n).aroots S = n • p.aroots S

Tactic:
rw [aroots_def, Polynomial.map_pow, roots_pow]

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem num_one : num (1 : RatFunc K) = 1

Proof state:
K : Type u
inst✝ : Field K
⊢ num 1 = 1

Tactic:
convert num_div (1 : K[X]) 1 <;> simp

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma not_dvd_of_pos_of_lt (h1 : 0 < n) (h2 : n < m) : ¬m ∣ n

Proof state:
case intro.inr
m k : ℕ
h1 : 0 < m * k
h2 : m * k < m
hk : k > 0
⊢ False

Tactic:
exact Nat.not_lt.2 (Nat.le_mul_of_pos_right _ hk) h2

Result:
no goals

Proof state:
case intro
m k : ℕ
h1 : 0 < m * k
h2 : m * k < m
⊢ False

Tactic:
rcases Nat.eq_zero_or_pos k with (rfl | hk)

Result:
case intro.inl
m : ℕ
h1 : 0 < m * 0
h2 : m * 0 < m
⊢ False

case intro.inr
m k : ℕ
h1 : 0 < m * k
h2 : m * k < m
hk : k > 0
⊢ False

Proof state:
m n : ℕ
h1 : 0 < n
h2 : n < m
⊢ ¬m ∣ n

Tactic:
rintro ⟨k, rfl⟩

Result:
case intro
m k : ℕ
h1 : 0 < m * k
h2 : m * k < m
⊢ False

Proof state:
case intro.inl
m : ℕ
h1 : 0 < m * 0
h2 : m * 0 < m
⊢ False

Tactic:
exact Nat.lt_irrefl 0 h1

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean
lemma shiftFunctorAdd_eq (a b : ℤ) :
    CategoryTheory.shiftFunctorAdd (CochainComplex C ℤ) a b = shiftFunctorAdd' C a b _ rfl

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
a b : ℤ
⊢ shiftFunctorAdd (CochainComplex C ℤ) a b = shiftFunctorAdd' C a b (a + b) ⋯

Tactic:
rw [← CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd'_eq]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
@[simp] lemma cast_nonpos : (q : K) ≤ 0 ↔ q ≤ 0

Proof state:
q : ℚ
K : Type u_5
inst✝ : LinearOrderedField K
⊢ ↑q ≤ 0 ↔ q ≤ 0

Tactic:
norm_cast

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
/-- The image of `ExteriorAlgebra.ιMulti R n` is contained in the `n`th exterior power. -/
lemma ιMulti_range (n : ℕ) :
    Set.range (ιMulti R n (M := M)) ⊆ ↑(⋀[R]^n M)

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ ∀ (y : Fin n → M), (ιMulti R n) y ∈ ↑(⋀[R]^n M)

Tactic:
intro v

Result:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n → M
⊢ (ιMulti R n) v ∈ ↑(⋀[R]^n M)

Proof state:
case a
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n → M
⊢ ∃ f, (List.ofFn fun i => ↑(f i)).prod = (List.ofFn fun i => (ι R) (v i)).prod

Tactic:
exact ⟨fun i => ⟨ι R (v i), LinearMap.mem_range_self _ _⟩, rfl⟩

Result:
no goals

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n → M
⊢ (List.ofFn fun i => (ι R) (v i)).prod ∈ ↑(⋀[R]^n M)

Tactic:
apply Submodule.pow_subset_pow

Result:
case a
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n → M
⊢ (List.ofFn fun i => (ι R) (v i)).prod ∈ ↑(LinearMap.range (ι R)) ^ n

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n → M
⊢ (ιMulti R n) v ∈ ↑(⋀[R]^n M)

Tactic:
rw [ιMulti_apply]

Result:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n → M
⊢ (List.ofFn fun i => (ι R) (v i)).prod ∈ ↑(⋀[R]^n M)

Proof state:
case a
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n → M
⊢ (List.ofFn fun i => (ι R) (v i)).prod ∈ ↑(LinearMap.range (ι R)) ^ n

Tactic:
rw [Set.mem_pow]

Result:
case a
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
v : Fin n → M
⊢ ∃ f, (List.ofFn fun i => ↑(f i)).prod = (List.ofFn fun i => (ι R) (v i)).prod

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ Set.range ⇑(ιMulti R n) ⊆ ↑(⋀[R]^n M)

Tactic:
rw [Set.range_subset_iff]

Result:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
n : ℕ
⊢ ∀ (y : Fin n → M), (ιMulti R n) y ∈ ↑(⋀[R]^n M)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem head_zipWithAll {f : Option α → Option β → γ} (h) :
    (zipWithAll f as bs).head h = f as.head? bs.head?

Proof state:
case x
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
h : zipWithAll f as bs ≠ []
⊢ some ((zipWithAll f as bs).head h) = some (f as.head? bs.head?)

Tactic:
rw [← head?_eq_head, head?_zipWithAll]

Result:
case x
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
h : zipWithAll f as bs ≠ []
⊢ (match as.head?, bs.head? with
    | none, none => none
    | a?, b? => some (f a? b?)) =
    some (f as.head? bs.head?)

Proof state:
case x
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
h : zipWithAll f as bs ≠ []
⊢ (match as.head?, bs.head? with
    | none, none => none
    | a?, b? => some (f a? b?)) =
    some (f as.head? bs.head?)

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
h : zipWithAll f as bs ≠ []
⊢ (zipWithAll f as bs).head h = f as.head? bs.head?

Tactic:
apply Option.some.inj

Result:
case x
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : Option α → Option β → γ
h : zipWithAll f as bs ≠ []
⊢ some ((zipWithAll f as bs).head h) = some (f as.head? bs.head?)
-- Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
theorem mul_nonneg_iff_of_pos_left [PosMulStrictMono α]
    (h : 0 < c) : 0 ≤ c * b ↔ 0 ≤ b

Proof state:
case h.e'_1.h.e'_3
α : Type u
inst✝² : Semiring α
inst✝¹ : LinearOrder α
b c : α
inst✝ : PosMulStrictMono α
h : 0 < c
⊢ 0 = c * 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
inst✝² : Semiring α
inst✝¹ : LinearOrder α
b c : α
inst✝ : PosMulStrictMono α
h : 0 < c
⊢ 0 ≤ c * b ↔ 0 ≤ b

Tactic:
convert mul_le_mul_left h

Result:
case h.e'_1.h.e'_3
α : Type u
inst✝² : Semiring α
inst✝¹ : LinearOrder α
b c : α
inst✝ : PosMulStrictMono α
h : 0 < c
⊢ 0 = c * 0
-- Mathlib/GroupTheory/GroupAction/FixedPoints.lean
theorem fixedBy_inv (g : G) : fixedBy α g⁻¹ = fixedBy α g

Proof state:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
x✝ : α
⊢ x✝ ∈ fixedBy α g⁻¹ ↔ x✝ ∈ fixedBy α g

Tactic:
rw [mem_fixedBy, mem_fixedBy, inv_smul_eq_iff, eq_comm]

Result:
no goals

Proof state:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
⊢ fixedBy α g⁻¹ = fixedBy α g

Tactic:
ext

Result:
case h
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
x✝ : α
⊢ x✝ ∈ fixedBy α g⁻¹ ↔ x✝ ∈ fixedBy α g
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem modify_eq_set_get (f : α → α) {n} {l : List α} (h) :
    l.modify f n = l.set n (f (l.get ⟨n, h⟩))

Proof state:
α : Type u_1
f : α → α
n : Nat
l : List α
h : n < l.length
⊢ modify f n l = l.set n (f (l.get ⟨n, h⟩))

Tactic:
rw [modify_eq_set_get?, get?_eq_get h]

Result:
α : Type u_1
f : α → α
n : Nat
l : List α
h : n < l.length
⊢ ((fun a => l.set n (f a)) <$> some (l.get ⟨n, h⟩)).getD l = l.set n (f (l.get ⟨n, h⟩))

Proof state:
α : Type u_1
f : α → α
n : Nat
l : List α
h : n < l.length
⊢ ((fun a => l.set n (f a)) <$> some (l.get ⟨n, h⟩)).getD l = l.set n (f (l.get ⟨n, h⟩))

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem prod_add_index_of_disjoint [AddCommMonoid M] {f1 f2 : α →₀ M}
    (hd : Disjoint f1.support f2.support) {β : Type*} [CommMonoid β] (g : α → M → β) :
    (f1 + f2).prod g = f1.prod g * f2.prod g

Proof state:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
this : ∀ {f1 f2 : α →₀ M}, Disjoint f1.support f2.support → ∏ x ∈ f1.support, g x (f1 x + f2 x) = f1.prod g
⊢ (f1 + f2).prod g = f1.prod g * f2.prod g

Tactic:
simp_rw [← this hd, ← this hd.symm, add_comm (f2 _), Finsupp.prod, support_add_eq hd,
prod_union hd, add_apply]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
this : ∀ {f1 f2 : α →₀ M}, Disjoint f1.support f2.support → ∏ x ∈ f1.support, g x (f1 x + f2 x) = f1.prod g
⊢ (f1 + f2).prod g = f1.prod g * f2.prod g

Tactic:
classical simp_rw [← this hd, ← this hd.symm, add_comm (f2 _), Finsupp.prod, support_add_eq hd,
    prod_union hd, add_apply]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
⊢ (f1 + f2).prod g = f1.prod g * f2.prod g

Tactic:
have :
  ∀ {f1 f2 : α →₀ M},
    Disjoint f1.support f2.support → (∏ x ∈ f1.support, g x (f1 x + f2 x)) = f1.prod g :=
  fun hd =>
  Finset.prod_congr rfl fun x hx => by
    simp only [not_mem_support_iff.mp (disjoint_left.mp hd hx), add_zero]

Result:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
this : ∀ {f1 f2 : α →₀ M}, Disjoint f1.support f2.support → ∏ x ∈ f1.support, g x (f1 x + f2 x) = f1.prod g
⊢ (f1 + f2).prod g = f1.prod g * f2.prod g

Proof state:
α : Type u_1
M : Type u_8
inst✝¹ : AddCommMonoid M
f1 f2 : α →₀ M
hd✝ : Disjoint f1.support f2.support
β : Type u_16
inst✝ : CommMonoid β
g : α → M → β
f1✝ f2✝ : α →₀ M
hd : Disjoint f1✝.support f2✝.support
x : α
hx : x ∈ f1✝.support
⊢ g x (f1✝ x + f2✝ x) = g x (f1✝ x)

Tactic:
simp only [not_mem_support_iff.mp (disjoint_left.mp hd hx), add_zero]

Result:
no goals
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem l_sup (gc : GaloisConnection l u) : l (a₁ ⊔ a₂) = l a₁ ⊔ l a₂ :=
  (gc.isLUB_l_image isLUB_pair).unique <| by simp only [image_pair, isLUB_pair]

Proof state:
α : Type u
β : Type v
a₁ a₂ : α
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
l : α → β
u : β → α
gc : GaloisConnection l u
⊢ IsLUB (l '' {a₁, a₂}) (l a₁ ⊔ l a₂)

Tactic:
simp only [image_pair, isLUB_pair]

Result:
no goals
-- Mathlib/FieldTheory/IsAlgClosed/Basic.lean
theorem exists_eq_mul_self [IsAlgClosed k] (x : k) : ∃ z, x = z * z

Proof state:
case intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
z : k
⊢ ∃ z_1, z ^ 2 = z_1 * z_1

Tactic:
exact ⟨z, sq z⟩

Result:
no goals

Proof state:
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
x : k
⊢ ∃ z, x = z * z

Tactic:
rcases exists_pow_nat_eq x zero_lt_two with ⟨z, rfl⟩

Result:
case intro
k : Type u
inst✝¹ : Field k
inst✝ : IsAlgClosed k
z : k
⊢ ∃ z_1, z ^ 2 = z_1 * z_1
-- Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
theorem Matrix.Represents.add {A A' : Matrix ι ι R} {f f' : Module.End R M} (h : A.Represents b f)
    (h' : Matrix.Represents b A' f') : (A + A').Represents b (f + f')

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : (PiToModule.fromMatrix R b) A = (PiToModule.fromEnd R b) f
h' : (PiToModule.fromMatrix R b) A' = (PiToModule.fromEnd R b) f'
⊢ (PiToModule.fromMatrix R b) (A + A') = (PiToModule.fromEnd R b) (f + f')

Tactic:
rw [map_add, map_add, h, h']

Result:
no goals

Proof state:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
⊢ Represents b (A + A') (f + f')

Tactic:
delta Matrix.Represents at h h' ⊢

Result:
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
b : ι → M
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : (PiToModule.fromMatrix R b) A = (PiToModule.fromEnd R b) f
h' : (PiToModule.fromMatrix R b) A' = (PiToModule.fromEnd R b) f'
⊢ (PiToModule.fromMatrix R b) (A + A') = (PiToModule.fromEnd R b) (f + f')
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem sumCoords_reindex : (b.reindex e).sumCoords = b.sumCoords

Proof state:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
e : ι ≃ ι'
x : M
⊢ ((mapDomain (⇑e) (b.repr x)).sum fun x => id) = (b.repr x).sum fun x => id

Tactic:
exact Finsupp.sum_mapDomain_index (fun _ => rfl) fun _ _ _ => rfl

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
e : ι ≃ ι'
⊢ (b.reindex e).sumCoords = b.sumCoords

Tactic:
ext x

Result:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
e : ι ≃ ι'
x : M
⊢ (b.reindex e).sumCoords x = b.sumCoords x

Proof state:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
e : ι ≃ ι'
x : M
⊢ (b.reindex e).sumCoords x = b.sumCoords x

Tactic:
simp only [coe_sumCoords, repr_reindex]

Result:
case h
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis ι R M
e : ι ≃ ι'
x : M
⊢ ((mapDomain (⇑e) (b.repr x)).sum fun x => id) = (b.repr x).sum fun x => id