harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem map_expand_pow_char (f : R[X]) (n : ℕ) :
    map (frobenius R p ^ n) (expand R (p ^ n) f) = f ^ p ^ n

Proof state:
case succ
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n✝ : ℕ
n_ih : map (frobenius R p ^ n✝) ((expand R (p ^ n✝)) f) = f ^ p ^ n✝
⊢ f ^ p ^ (n✝ + 1) = map (frobenius R p ^ (n✝ + 1)) ((expand R (p ^ (n✝ + 1))) f)

Tactic:
rw [pow_succ, pow_mul, ← n_ih, ← expand_char, pow_succ', RingHom.mul_def, ← map_map, mul_comm,
  expand_mul, ← map_expand]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n✝ : ℕ
n_ih : map (frobenius R p ^ n✝) ((expand R (p ^ n✝)) f) = f ^ p ^ n✝
⊢ map (frobenius R p ^ (n✝ + 1)) ((expand R (p ^ (n✝ + 1))) f) = f ^ p ^ (n✝ + 1)

Tactic:
symm

Result:
case succ
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n✝ : ℕ
n_ih : map (frobenius R p ^ n✝) ((expand R (p ^ n✝)) f) = f ^ p ^ n✝
⊢ f ^ p ^ (n✝ + 1) = map (frobenius R p ^ (n✝ + 1)) ((expand R (p ^ (n✝ + 1))) f)

Proof state:
case zero
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
⊢ map (frobenius R p ^ 0) ((expand R (p ^ 0)) f) = f ^ p ^ 0

Tactic:
simp [RingHom.one_def]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommSemiring R
p : ℕ
inst✝ : ExpChar R p
f : R[X]
n : ℕ
⊢ map (frobenius R p ^ n) ((expand R (p ^ n)) f) = f ^ p ^ n

Tactic:
induction n with
| zero => simp [RingHom.one_def]
| succ _ n_ih =>
  symm
  rw [pow_succ, pow_mul, ← n_ih, ← expand_char, pow_succ', RingHom.mul_def, ← map_map, mul_comm,
    expand_mul, ← map_expand]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem max_eq_left {a b : Nat} (h : b ≤ a) : max a b = a

Proof state:
a b : Nat
h : b ≤ a
⊢ max b a = a

Tactic:
exact Nat.max_eq_right h

Result:
no goals

Proof state:
a b : Nat
h : b ≤ a
⊢ max a b = a

Tactic:
rw [Nat.max_comm]

Result:
a b : Nat
h : b ≤ a
⊢ max b a = a
-- Mathlib/RingTheory/Nilpotent/Defs.lean
theorem isNilpotent_mul_right (h_comm : Commute x y) (h : IsNilpotent y) : IsNilpotent (x * y)

Proof state:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
h : IsNilpotent y
⊢ IsNilpotent (x * y)

Tactic:
rw [h_comm.eq]

Result:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
h : IsNilpotent y
⊢ IsNilpotent (y * x)

Proof state:
R : Type u_1
x y : R
inst✝ : Semiring R
h_comm : Commute x y
h : IsNilpotent y
⊢ IsNilpotent (y * x)

Tactic:
exact h_comm.symm.isNilpotent_mul_left h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem tan_pi : tan π = 0

Proof state:
⊢ tan π = 0

Tactic:
rw [tan_periodic.eq, tan_zero]

Result:
no goals
-- Mathlib/Algebra/Ring/CentroidHom.lean
theorem comp_mul_comm (T S : CentroidHom α) (a b : α) : (T ∘ S) (a * b) = (S ∘ T) (a * b)

Proof state:
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
⊢ T (S (a * b)) = S (T (a * b))

Tactic:
rw [map_mul_right, map_mul_left, ← map_mul_right, ← map_mul_left]

Result:
no goals

Proof state:
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
⊢ (⇑T ∘ ⇑S) (a * b) = (⇑S ∘ ⇑T) (a * b)

Tactic:
simp only [Function.comp_apply]

Result:
α : Type u_5
inst✝ : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
⊢ T (S (a * b)) = S (T (a * b))
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
@[simp]
lemma spanningCoe_subgraphOfAdj {v w : V} (hadj : G.Adj v w) :
    (G.subgraphOfAdj hadj).spanningCoe = fromEdgeSet {s(v, w)}

Proof state:
V : Type u
G : SimpleGraph V
v w : V
hadj : G.Adj v w
⊢ (G.subgraphOfAdj hadj).spanningCoe = fromEdgeSet {s(v, w)}

Tactic:
ext v w

Result:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
v✝ w✝ : V
hadj : G.Adj v✝ w✝
v w : V
⊢ (G.subgraphOfAdj hadj).spanningCoe.Adj v w ↔ (fromEdgeSet {s(v✝, w✝)}).Adj v w

Proof state:
case Adj.h.h.a
V : Type u
G : SimpleGraph V
v✝ w✝ : V
hadj : G.Adj v✝ w✝
v w : V
⊢ (G.subgraphOfAdj hadj).spanningCoe.Adj v w ↔ (fromEdgeSet {s(v✝, w✝)}).Adj v w

Tactic:
aesop

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_const [IsFiniteMeasure μ] (hT : DominatedFinMeasAdditive μ T C) (x : E) :
    (setToFun μ T hT fun _ => x) = T univ x

Proof state:
α : 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 α
inst✝¹ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
inst✝ : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
this : (fun x_1 => x) = Set.univ.indicator fun x_1 => x
⊢ (setToFun μ T hT fun x_1 => x) = (T Set.univ) x

Tactic:
rw [this]

Result:
α : 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 α
inst✝¹ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
inst✝ : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
this : (fun x_1 => x) = Set.univ.indicator fun x_1 => x
⊢ setToFun μ T hT (Set.univ.indicator fun x_1 => x) = (T Set.univ) x

Proof state:
α : 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 α
inst✝¹ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
inst✝ : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
this : (fun x_1 => x) = Set.univ.indicator fun x_1 => x
⊢ setToFun μ T hT (Set.univ.indicator fun x_1 => x) = (T Set.univ) x

Tactic:
exact setToFun_indicator_const hT MeasurableSet.univ (measure_ne_top _ _) x

Result:
no goals

Proof state:
α : 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 α
inst✝¹ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
inst✝ : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
⊢ (setToFun μ T hT fun x_1 => x) = (T Set.univ) x

Tactic:
have : (fun _ : α => x) = Set.indicator univ fun _ => x := (indicator_univ _).symm

Result:
α : 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 α
inst✝¹ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
inst✝ : IsFiniteMeasure μ
hT : DominatedFinMeasAdditive μ T C
x : E
this : (fun x_1 => x) = Set.univ.indicator fun x_1 => x
⊢ (setToFun μ T hT fun x_1 => x) = (T Set.univ) x
-- Mathlib/Geometry/Euclidean/PerpBisector.lean
theorem perpBisector_comm (p₁ p₂ : P) : perpBisector p₁ p₂ = perpBisector p₂ p₁

Proof state:
case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ c : P
⊢ c ∈ perpBisector p₁ p₂ ↔ c ∈ perpBisector p₂ p₁

Tactic:
simp only [mem_perpBisector_iff_dist_eq, eq_comm]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ : P
⊢ perpBisector p₁ p₂ = perpBisector p₂ p₁

Tactic:
ext c

Result:
case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ c : P
⊢ c ∈ perpBisector p₁ p₂ ↔ c ∈ perpBisector p₂ p₁
-- Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
theorem ContMDiffWithinAt.of_le (hf : ContMDiffWithinAt I I' n f s x) (le : m ≤ n) :
    ContMDiffWithinAt I I' m f s x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
m n : WithTop ℕ∞
hf : ContMDiffWithinAt I I' n f s x
le : m ≤ n
⊢ ContMDiffWithinAt I I' m f s x

Tactic:
simp only [ContMDiffWithinAt, LiftPropWithinAt] at hf ⊢

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
m n : WithTop ℕ∞
hf : LiftPropWithinAt (ContDiffWithinAtProp I I' n) f s x
le : m ≤ n
⊢ LiftPropWithinAt (ContDiffWithinAtProp I I' m) f s x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
s : Set M
x : M
m n : WithTop ℕ∞
hf : LiftPropWithinAt (ContDiffWithinAtProp I I' n) f s x
le : m ≤ n
⊢ LiftPropWithinAt (ContDiffWithinAtProp I I' m) f s x

Tactic:
exact ⟨hf.1, hf.2.of_le (mod_cast le)⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem sameRay_neg_smul_right_iff {v : M} {r : R} : SameRay R (-v) (r • v) ↔ r ≤ 0 ∨ v = 0

Proof state:
R : Type u_1
inst✝³ : LinearOrderedCommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
v : M
r : R
⊢ SameRay R (-v) (r • v) ↔ r ≤ 0 ∨ v = 0

Tactic:
rw [← sameRay_neg_iff, neg_neg, ← neg_smul, sameRay_smul_right_iff, neg_nonneg]

Result:
no goals
-- Mathlib/NumberTheory/FunctionField.lean
theorem inftyValuation_of_nonzero {x : RatFunc Fq} (hx : x ≠ 0) :
    inftyValuationDef Fq x = Multiplicative.ofAdd x.intDegree

Proof state:
Fq : Type u_1
inst✝¹ : Field Fq
inst✝ : DecidableEq (RatFunc Fq)
x : RatFunc Fq
hx : x ≠ 0
⊢ inftyValuationDef Fq x = ↑(Multiplicative.ofAdd x.intDegree)

Tactic:
rw [inftyValuationDef, if_neg hx]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem Basis.det_comp_basis [Module A M'] (b : Basis ι A M) (b' : Basis ι A M') (f : M →ₗ[A] M') :
    b'.det (f ∘ b) = LinearMap.det (f ∘ₗ (b'.equiv b (Equiv.refl ι) : M' →ₗ[A] M))

Proof state:
M : Type u_2
inst✝⁶ : AddCommGroup M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ (b'.toMatrix (⇑f ∘ ⇑b)).det = ((LinearMap.toMatrix b b') f).det

Tactic:
congr 1

Result:
case e_M
M : Type u_2
inst✝⁶ : AddCommGroup M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ b'.toMatrix (⇑f ∘ ⇑b) = (LinearMap.toMatrix b b') f

Proof state:
M : Type u_2
inst✝⁶ : AddCommGroup M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ b'.det (⇑f ∘ ⇑b) = LinearMap.det (f ∘ₗ ↑(b'.equiv b (Equiv.refl ι)))

Tactic:
rw [Basis.det_apply, ← LinearMap.det_toMatrix b', LinearMap.toMatrix_comp _ b, Matrix.det_mul,
  LinearMap.toMatrix_basis_equiv, Matrix.det_one, mul_one]

Result:
M : Type u_2
inst✝⁶ : AddCommGroup M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ (b'.toMatrix (⇑f ∘ ⇑b)).det = ((LinearMap.toMatrix b b') f).det

Proof state:
case e_M.a
M : Type u_2
inst✝⁶ : AddCommGroup M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
i j : ι
⊢ b'.toMatrix (⇑f ∘ ⇑b) i j = (LinearMap.toMatrix b b') f i j

Tactic:
rw [Basis.toMatrix_apply, LinearMap.toMatrix_apply, Function.comp_apply]

Result:
no goals

Proof state:
case e_M
M : Type u_2
inst✝⁶ : AddCommGroup M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
⊢ b'.toMatrix (⇑f ∘ ⇑b) = (LinearMap.toMatrix b b') f

Tactic:
ext i j

Result:
case e_M.a
M : Type u_2
inst✝⁶ : AddCommGroup M
M' : Type u_3
inst✝⁵ : AddCommGroup M'
ι : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : Fintype ι
A : Type u_5
inst✝² : CommRing A
inst✝¹ : Module A M
inst✝ : Module A M'
b : Basis ι A M
b' : Basis ι A M'
f : M →ₗ[A] M'
i j : ι
⊢ b'.toMatrix (⇑f ∘ ⇑b) i j = (LinearMap.toMatrix b b') f i j
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem mem_coclosedLindelof : s ∈ coclosedLindelof X ↔
    ∃ t, IsClosed t ∧ IsLindelof t ∧ tᶜ ⊆ s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ s ∈ coclosedLindelof X ↔ ∃ t, IsClosed t ∧ IsLindelof t ∧ tᶜ ⊆ s

Tactic:
simp only [hasBasis_coclosedLindelof.mem_iff, and_assoc]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem le_measure_diff : μ s₁ - μ s₂ ≤ μ (s₁ \ s₂) :=
  tsub_le_iff_left.2 <| (measure_le_inter_add_diff μ s₁ s₂).trans <| by
    gcongr; apply inter_subset_right

Proof state:
case bc.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
⊢ s₁ ∩ s₂ ⊆ s₂

Tactic:
apply inter_subset_right

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
⊢ μ (s₁ ∩ s₂) + μ (s₁ \ s₂) ≤ μ s₂ + μ (s₁ \ s₂)

Tactic:
gcongr

Result:
case bc.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
⊢ s₁ ∩ s₂ ⊆ s₂
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem xn_modEq_x4n_sub {n j} (h : j ≤ 2 * n) : xn a1 (4 * n - j) ≡ xn a1 j [MOD xn a1 n] :=
  have h' : j ≤ 2 * n := le_trans h (by rw [Nat.succ_mul])
  ModEq.add_right_cancel' (xn a1 (2 * n - j)) <| by
    refine @ModEq.trans _ _ 0 _ ?_ (by rw [add_comm]; exact (xn_modEq_x2n_sub _ h).symm)
    rw [show 4 * n = 2 * n + 2 * n from right_distrib 2 2 n, add_tsub_assoc_of_le h']
    apply xn_modEq_x2n_add

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (4 * n - j) + xn a1 (2 * n - j) ≡ xn a1 j + xn a1 (2 * n - j) [MOD xn a1 n]

Tactic:
refine @ModEq.trans _ _ 0 _ ?_ (by rw [add_comm]; exact (xn_modEq_x2n_sub _ h).symm)

Result:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (4 * n - j) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (4 * n - j) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]

Tactic:
rw [show 4 * n = 2 * n + 2 * n from right_distrib 2 2 n, add_tsub_assoc_of_le h']

Result:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (2 * n + (2 * n - j)) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (2 * n + (2 * n - j)) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]

Tactic:
apply xn_modEq_x2n_add

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ 0 ≡ xn a1 (2 * n - j) + xn a1 j [MOD xn a1 n]

Tactic:
exact (xn_modEq_x2n_sub _ h).symm

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
⊢ 2 * n ≤ 2 * n

Tactic:
rw [Nat.succ_mul]

Result:
no goals

Proof state:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ 0 ≡ xn a1 j + xn a1 (2 * n - j) [MOD xn a1 n]

Tactic:
rw [add_comm]

Result:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ 0 ≡ xn a1 (2 * n - j) + xn a1 j [MOD xn a1 n]
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem nadd_nmul (a b c) : (a ♯ b) ⨳ c = a ⨳ c ♯ b ⨳ c

Proof state:
a b c : Ordinal.{u_1}
⊢ (a ♯ b) ⨳ c = a ⨳ c ♯ b ⨳ c

Tactic:
rw [nmul_comm, nmul_nadd, nmul_comm, nmul_comm c]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem set_getElem_self {as : Array α} {i : Nat} (h : i < as.size) :
    as.set i as[i] = as

Proof state:
case mk
α : Type u_1
i : Nat
toList✝ : List α
h : i < { toList := toList✝ }.size
⊢ { toList := toList✝ }.set i { toList := toList✝ }[i] h = { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
as : Array α
i : Nat
h : i < as.size
⊢ as.set i as[i] h = as

Tactic:
cases as

Result:
case mk
α : Type u_1
i : Nat
toList✝ : List α
h : i < { toList := toList✝ }.size
⊢ { toList := toList✝ }.set i { toList := toList✝ }[i] h = { toList := toList✝ }
-- Mathlib/Data/List/Sigma.lean
theorem keys_kerase {a} {l : List (Sigma β)} : (kerase a l).keys = l.keys.erase a

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ map Sigma.fst (eraseP (fun s => decide (a = s.fst)) l) = map Sigma.fst (eraseP (fun x => a == x.fst) l)

Tactic:
congr

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ (kerase a l).keys = l.keys.erase a

Tactic:
rw [keys, kerase, erase_eq_eraseP, eraseP_map, Function.comp_def]

Result:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
⊢ map Sigma.fst (eraseP (fun s => decide (a = s.fst)) l) = map Sigma.fst (eraseP (fun x => a == x.fst) l)
-- Mathlib/NumberTheory/Divisors.lean
theorem image_fst_divisorsAntidiagonal : (divisorsAntidiagonal n).image Prod.fst = divisors n

Proof state:
case h
n a✝ : ℕ
⊢ a✝ ∈ image Prod.fst n.divisorsAntidiagonal ↔ a✝ ∈ n.divisors

Tactic:
simp [Dvd.dvd, @eq_comm _ n (_ * _)]

Result:
no goals

Proof state:
n : ℕ
⊢ image Prod.fst n.divisorsAntidiagonal = n.divisors

Tactic:
ext

Result:
case h
n a✝ : ℕ
⊢ a✝ ∈ image Prod.fst n.divisorsAntidiagonal ↔ a✝ ∈ n.divisors
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem iterate_verschiebung_coeff (x : 𝕎 R) (n k : ℕ) :
    (verschiebung^[n] x).coeff (k + n) = x.coeff k

Proof state:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ k : ℕ
ih : ((⇑verschiebung)^[k] x).coeff (k✝ + k) = x.coeff k✝
⊢ ((⇑verschiebung)^[k + 1] x).coeff (k✝ + (k + 1)) = x.coeff k✝

Tactic:
rw [iterate_succ_apply', Nat.add_succ, verschiebung_coeff_succ]

Result:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ k : ℕ
ih : ((⇑verschiebung)^[k] x).coeff (k✝ + k) = x.coeff k✝
⊢ ((⇑verschiebung)^[k] x).coeff (k✝ + k) = x.coeff k✝

Proof state:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
⊢ ((⇑verschiebung)^[0] x).coeff (k + 0) = x.coeff k

Tactic:
simp

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n k : ℕ
⊢ ((⇑verschiebung)^[n] x).coeff (k + n) = x.coeff k

Tactic:
induction' n with k ih

Result:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k : ℕ
⊢ ((⇑verschiebung)^[0] x).coeff (k + 0) = x.coeff k

case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ k : ℕ
ih : ((⇑verschiebung)^[k] x).coeff (k✝ + k) = x.coeff k✝
⊢ ((⇑verschiebung)^[k + 1] x).coeff (k✝ + (k + 1)) = x.coeff k✝

Proof state:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
k✝ k : ℕ
ih : ((⇑verschiebung)^[k] x).coeff (k✝ + k) = x.coeff k✝
⊢ ((⇑verschiebung)^[k] x).coeff (k✝ + k) = x.coeff k✝

Tactic:
exact ih

Result:
no goals
-- Mathlib/SetTheory/Nimber/Field.lean
theorem mul_one (a : Nimber) : a * 1 = a

Proof state:
a : Nimber
⊢ a * 1 = a

Tactic:
rw [Nimber.mul_comm, Nimber.one_mul]

Result:
no goals
-- Mathlib/Data/Finsupp/NeLocus.lean
theorem neLocus_eq_support_sub : f.neLocus g = (f - g).support

Proof state:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f g : α →₀ N
⊢ f.neLocus g = (f - g).support

Tactic:
rw [← neLocus_add_right _ _ (-g), add_neg_cancel, neLocus_zero_right, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Order/Interval/Set/ProjIcc.lean
theorem projIcc_of_right_le (hx : b ≤ x) : projIcc a b h x = ⟨b, right_mem_Icc.2 h⟩

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : b ≤ x
⊢ projIcc a b h x = ⟨b, ⋯⟩

Tactic:
simp [projIcc, hx, h]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[bound]
protected lemma Bound.one_lt_mul : 1 ≤ a ∧ 1 < b ∨ 1 < a ∧ 1 ≤ b → 1 < a * b

Proof state:
case inl.intro
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a b : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 1 ≤ a
hb : 1 < b
⊢ 1 < a * b

case inr.intro
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a b : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 1 < a
hb : 1 ≤ b
⊢ 1 < a * b

Tactic:
exacts [one_lt_mul ha hb, one_lt_mul_of_lt_of_le ha hb]

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a b : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
⊢ 1 ≤ a ∧ 1 < b ∨ 1 < a ∧ 1 ≤ b → 1 < a * b

Tactic:
rintro (⟨ha, hb⟩ | ⟨ha, hb⟩)

Result:
case inl.intro
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a b : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 1 ≤ a
hb : 1 < b
⊢ 1 < a * b

case inr.intro
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a b : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
ha : 1 < a
hb : 1 ≤ b
⊢ 1 < a * b
-- Mathlib/Probability/Martingale/Basic.lean
theorem Supermartingale.le_zero_of_predictable [Preorder E] [SigmaFiniteFiltration μ 𝒢]
    {f : ℕ → Ω → E} (hfmgle : Supermartingale f 𝒢 μ) (hfadp : Adapted 𝒢 fun n => f (n + 1))
    (n : ℕ) : f n ≤ᵐ[μ] f 0

Proof state:
case zero
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
𝒢 : Filtration ℕ m0
inst✝¹ : Preorder E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Supermartingale f 𝒢 μ
hfadp : Adapted 𝒢 fun n => f (n + 1)
⊢ f 0 ≤ᶠ[ae μ] f 0

Tactic:
rfl

Result:
no goals

Proof state:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
𝒢 : Filtration ℕ m0
inst✝¹ : Preorder E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Supermartingale f 𝒢 μ
hfadp : Adapted 𝒢 fun n => f (n + 1)
n : ℕ
⊢ f n ≤ᶠ[ae μ] f 0

Tactic:
induction' n with k ih

Result:
case zero
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
𝒢 : Filtration ℕ m0
inst✝¹ : Preorder E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Supermartingale f 𝒢 μ
hfadp : Adapted 𝒢 fun n => f (n + 1)
⊢ f 0 ≤ᶠ[ae μ] f 0

case succ
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
𝒢 : Filtration ℕ m0
inst✝¹ : Preorder E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Supermartingale f 𝒢 μ
hfadp : Adapted 𝒢 fun n => f (n + 1)
k : ℕ
ih : f k ≤ᶠ[ae μ] f 0
⊢ f (k + 1) ≤ᶠ[ae μ] f 0

Proof state:
case succ
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
𝒢 : Filtration ℕ m0
inst✝¹ : Preorder E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Supermartingale f 𝒢 μ
hfadp : Adapted 𝒢 fun n => f (n + 1)
k : ℕ
ih : f k ≤ᶠ[ae μ] f 0
⊢ f (k + 1) ≤ᶠ[ae μ] f 0

Tactic:
exact ((Germ.coe_eq.mp <| congr_arg Germ.ofFun <| condExp_of_stronglyMeasurable (𝒢.le _)
  (hfadp _) <| hfmgle.integrable _).symm.trans_le (hfmgle.2.1 k (k + 1) k.le_succ)).trans ih

Result:
no goals