harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean
lemma norm_equiv_le_norm_pi (x : C⋆ᵐᵒᵈ (Π i, E i)) : ‖equiv _ x‖ ≤ ‖x‖

Proof state:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
⊢ ‖(equiv ((i : ι) → E i)) x‖ ≤ ‖x‖

Tactic:
let _ : NormedAddCommGroup (C⋆ᵐᵒᵈ (Π i, E i)) := normedAddCommGroup

Result:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ ‖(equiv ((i : ι) → E i)) x‖ ≤ ‖x‖

Proof state:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ ‖(equiv ((i : ι) → E i)) x‖ ≤ ‖x‖

Tactic:
rw [pi_norm_le_iff_of_nonneg (by positivity)]

Result:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ ∀ (i : ι), ‖(equiv ((i : ι) → E i)) x i‖ ≤ ‖x‖

Proof state:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ 0 ≤ ‖x‖

Tactic:
positivity

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
x✝ : NormedAddCommGroup (C⋆ᵐᵒᵈ ((i : ι) → E i)) := normedAddCommGroup
⊢ ∀ (i : ι), ‖(equiv ((i : ι) → E i)) x i‖ ≤ ‖x‖

Tactic:
simpa using norm_apply_le_norm x

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_div_two_eq_sqrt {x : ℝ} (r : ℝ) (hx : 0 ≤ x) : x ^ (r / 2) = √x ^ r

Proof state:
x r : ℝ
hx : 0 ≤ x
⊢ x ^ (r / 2) = x ^ (1 / 2 * r)

Tactic:
congr

Result:
case e_a
x r : ℝ
hx : 0 ≤ x
⊢ r / 2 = 1 / 2 * r

Proof state:
case e_a
x r : ℝ
hx : 0 ≤ x
⊢ r / 2 = 1 / 2 * r

Tactic:
ring

Result:
no goals

Proof state:
x r : ℝ
hx : 0 ≤ x
⊢ x ^ (r / 2) = √x ^ r

Tactic:
rw [sqrt_eq_rpow, ← rpow_mul hx]

Result:
x r : ℝ
hx : 0 ≤ x
⊢ x ^ (r / 2) = x ^ (1 / 2 * r)
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem annihilator_span_singleton (g : M) :
    (Submodule.span R {g}).annihilator = ker (toSpanSingleton R M g)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : M
⊢ (span R {g}).annihilator = ker (toSpanSingleton R M g)

Tactic:
simp [annihilator_span]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_eq_of_bijOn {s : Set α} {t : Set β} {f : α → M} {g : β → M} (e : α → β)
    (he₀ : s.BijOn e t) (he₁ : ∀ x ∈ s, f x = g (e x)) : ∏ᶠ i ∈ s, f i = ∏ᶠ j ∈ t, g j

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Set α
t : Set β
f : α → M
g : β → M
e : α → β
he₀ : BijOn e s t
he₁ : ∀ x ∈ s, f x = g (e x)
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (j : α) (_ : j ∈ s), g (e j)

Tactic:
exact finprod_mem_congr rfl he₁

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Set α
t : Set β
f : α → M
g : β → M
e : α → β
he₀ : BijOn e s t
he₁ : ∀ x ∈ s, f x = g (e x)
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (j : β) (_ : j ∈ t), g j

Tactic:
rw [← Set.BijOn.image_eq he₀, finprod_mem_image he₀.2.1]

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
s : Set α
t : Set β
f : α → M
g : β → M
e : α → β
he₀ : BijOn e s t
he₁ : ∀ x ∈ s, f x = g (e x)
⊢ ∏ᶠ (i : α) (_ : i ∈ s), f i = ∏ᶠ (j : α) (_ : j ∈ s), g (e j)
-- Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
lemma prod_apply_symm (s : Set (α × β)) (s_mble : MeasurableSet s) :
    μ.prod ν s = ENNReal.toNNReal (∫⁻ y, μ.toMeasure ((fun x ↦ ⟨x, y⟩) ⁻¹' s) ∂ν)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
s : Set (α × β)
s_mble : MeasurableSet s
⊢ (μ.prod ν) s = (∫⁻ (y : β), ↑μ ((fun x => (x, y)) ⁻¹' s) ∂↑ν).toNNReal

Tactic:
simp [coeFn_def, Measure.prod_apply_symm s_mble]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem iterate_verschiebung_iterate_frobenius (x : 𝕎 R) (n : ℕ) :
    verschiebung^[n] (frobenius^[n] x) = x * (p ^ n)

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
⊢ (⇑verschiebung ∘ ⇑frobenius)^[n] x = x * ↑p ^ n

Tactic:
induction' n with n ih

Result:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ (⇑verschiebung ∘ ⇑frobenius)^[0] x = x * ↑p ^ 0

case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : (⇑verschiebung ∘ ⇑frobenius)^[n] x = x * ↑p ^ n
⊢ (⇑verschiebung ∘ ⇑frobenius)^[n + 1] x = x * ↑p ^ (n + 1)

Proof state:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : (⇑verschiebung ∘ ⇑frobenius)^[n] x = x * ↑p ^ n
⊢ (⇑verschiebung ∘ ⇑frobenius)^[n + 1] x = x * ↑p ^ (n + 1)

Tactic:
rw [iterate_succ_apply', ih, pow_succ, comp_apply, verschiebung_frobenius, mul_assoc]

Result:
no goals

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
⊢ (⇑verschiebung)^[n] ((⇑frobenius)^[n] x) = x * ↑p ^ n

Tactic:
rw [← comp_apply (f := verschiebung^[n]),
    ← Function.Commute.comp_iterate verschiebung_frobenius_comm]

Result:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
⊢ (⇑verschiebung ∘ ⇑frobenius)^[n] x = x * ↑p ^ n

Proof state:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ (⇑verschiebung ∘ ⇑frobenius)^[0] x = x * ↑p ^ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem roth_lower_bound : (N : ℝ) * exp (-4 * √(log N)) ≤ rothNumberNat N

Proof state:
case inr
N : ℕ
hN : N > 0
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑(rothNumberNat N)

Tactic:
obtain h₁ | h₁ := le_or_lt 4096 N

Result:
case inr.inl
N : ℕ
hN : N > 0
h₁ : 4096 ≤ N
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑(rothNumberNat N)

case inr.inr
N : ℕ
hN : N > 0
h₁ : N < 4096
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑(rothNumberNat N)

Proof state:
N : ℕ
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑(rothNumberNat N)

Tactic:
obtain rfl | hN := Nat.eq_zero_or_pos N

Result:
case inl

⊢ ↑0 * rexp (-4 * √(log ↑0)) ≤ ↑(rothNumberNat 0)

case inr
N : ℕ
hN : N > 0
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑(rothNumberNat N)

Proof state:
case inr.inr
N : ℕ
hN : N > 0
h₁ : N < 4096
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑(rothNumberNat N)

Tactic:
apply (lower_bound_le_one hN h₁.le).trans

Result:
case inr.inr
N : ℕ
hN : N > 0
h₁ : N < 4096
⊢ 1 ≤ ↑(rothNumberNat N)

Proof state:
case inr.inr
N : ℕ
hN : N > 0
h₁ : N < 4096
⊢ 1 ≤ ↑(rothNumberNat N)

Tactic:
simpa using rothNumberNat.monotone hN

Result:
no goals

Proof state:
case inl

⊢ ↑0 * rexp (-4 * √(log ↑0)) ≤ ↑(rothNumberNat 0)

Tactic:
norm_num

Result:
no goals

Proof state:
case inr.inl
N : ℕ
hN : N > 0
h₁ : 4096 ≤ N
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ ↑(rothNumberNat N)

Tactic:
exact (roth_lower_bound_explicit h₁).le

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Affine.lean
lemma isAffineHom_of_forall_exists_isAffineOpen
    (H : ∀ x : Y, ∃ U : Y.Opens, x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)) :
    IsAffineHom f

Proof state:
X Y : Scheme
f : X ⟶ Y
U : ↑↑Y.toPresheafedSpace → Y.Opens
hxU : ∀ (x : ↑↑Y.toPresheafedSpace), x ∈ U x
hU : ∀ (x : ↑↑Y.toPresheafedSpace), IsAffineOpen (U x)
hfU : ∀ (x : ↑↑Y.toPresheafedSpace), IsAffineOpen (f ⁻¹ᵁ U x)
x : ↑↑Y.toPresheafedSpace
x✝ : x ∈ ↑⊤
⊢ x ∈ ↑(⨆ i, ↑⟨U i, ⋯⟩)

Tactic:
simpa using ⟨x, hxU x⟩

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
H : ∀ (x : ↑↑Y.toPresheafedSpace), ∃ U, x ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
⊢ IsAffineHom f

Tactic:
choose U hxU hU hfU using H

Result:
X Y : Scheme
f : X ⟶ Y
U : ↑↑Y.toPresheafedSpace → Y.Opens
hxU : ∀ (x : ↑↑Y.toPresheafedSpace), x ∈ U x
hU : ∀ (x : ↑↑Y.toPresheafedSpace), IsAffineOpen (U x)
hfU : ∀ (x : ↑↑Y.toPresheafedSpace), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ IsAffineHom f

Proof state:
X Y : Scheme
f : X ⟶ Y
U : ↑↑Y.toPresheafedSpace → Y.Opens
hxU : ∀ (x : ↑↑Y.toPresheafedSpace), x ∈ U x
hU : ∀ (x : ↑↑Y.toPresheafedSpace), IsAffineOpen (U x)
hfU : ∀ (x : ↑↑Y.toPresheafedSpace), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ IsAffineHom f

Tactic:
rw [HasAffineProperty.iff_of_iSup_eq_top (P := @IsAffineHom) fun i ↦ ⟨U i, hU i⟩]

Result:
X Y : Scheme
f : X ⟶ Y
U : ↑↑Y.toPresheafedSpace → Y.Opens
hxU : ∀ (x : ↑↑Y.toPresheafedSpace), x ∈ U x
hU : ∀ (x : ↑↑Y.toPresheafedSpace), IsAffineOpen (U x)
hfU : ∀ (x : ↑↑Y.toPresheafedSpace), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ ∀ (i : ↑↑Y.toPresheafedSpace), IsAffine ↑(f ⁻¹ᵁ ↑⟨U i, ⋯⟩)

X Y : Scheme
f : X ⟶ Y
U : ↑↑Y.toPresheafedSpace → Y.Opens
hxU : ∀ (x : ↑↑Y.toPresheafedSpace), x ∈ U x
hU : ∀ (x : ↑↑Y.toPresheafedSpace), IsAffineOpen (U x)
hfU : ∀ (x : ↑↑Y.toPresheafedSpace), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ ⨆ i, ↑⟨U i, ⋯⟩ = ⊤

Proof state:
X Y : Scheme
f : X ⟶ Y
U : ↑↑Y.toPresheafedSpace → Y.Opens
hxU : ∀ (x : ↑↑Y.toPresheafedSpace), x ∈ U x
hU : ∀ (x : ↑↑Y.toPresheafedSpace), IsAffineOpen (U x)
hfU : ∀ (x : ↑↑Y.toPresheafedSpace), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ ⨆ i, ↑⟨U i, ⋯⟩ = ⊤

Tactic:
exact top_le_iff.mp (fun x _ ↦ by simpa using ⟨x, hxU x⟩)

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
U : ↑↑Y.toPresheafedSpace → Y.Opens
hxU : ∀ (x : ↑↑Y.toPresheafedSpace), x ∈ U x
hU : ∀ (x : ↑↑Y.toPresheafedSpace), IsAffineOpen (U x)
hfU : ∀ (x : ↑↑Y.toPresheafedSpace), IsAffineOpen (f ⁻¹ᵁ U x)
⊢ ∀ (i : ↑↑Y.toPresheafedSpace), IsAffine ↑(f ⁻¹ᵁ ↑⟨U i, ⋯⟩)

Tactic:
exact hfU

Result:
no goals
-- Mathlib/Topology/OmegaCompletePartialOrder.lean
theorem isωSup_ωSup {α} [OmegaCompletePartialOrder α] (c : Chain α) : IsωSup c (ωSup c)

Proof state:
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ IsωSup c (ωSup c)

Tactic:
constructor

Result:
case left
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (i : ℕ), c i ≤ ωSup c

case right
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (y : α), (∀ (i : ℕ), c i ≤ y) → ωSup c ≤ y

Proof state:
case left
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (i : ℕ), c i ≤ ωSup c

Tactic:
apply le_ωSup

Result:
no goals

Proof state:
case right
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (y : α), (∀ (i : ℕ), c i ≤ y) → ωSup c ≤ y

Tactic:
apply ωSup_le

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem factors_of_le {Y Z : C} {P Q : Subobject Y} (f : Z ⟶ Y) (h : P ≤ Q) :
    P.Factors f → Q.Factors f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
⊢ (representative.obj P).Factors f → (representative.obj Q).Factors f

Tactic:
exact fun ⟨u, hu⟩ => ⟨u ≫ ofLE _ _ h, by simp [← hu]⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
⊢ P.Factors f → Q.Factors f

Tactic:
simp only [factors_iff]

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
⊢ (representative.obj P).Factors f → (representative.obj Q).Factors f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
x✝ : (representative.obj P).Factors f
u : Z ⟶ (representative.obj P).obj.left
hu : u ≫ (representative.obj P).arrow = f
⊢ (u ≫ P.ofLE Q h) ≫ (representative.obj Q).arrow = f

Tactic:
simp [← hu]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_mul_natCast (x : ℝ≥0∞) (y : ℝ) (n : ℕ) : x ^ (y * n) = (x ^ y) ^ n

Proof state:
x : ℝ≥0∞
y : ℝ
n : ℕ
⊢ x ^ (y * ↑n) = (x ^ y) ^ n

Tactic:
rw [rpow_mul, rpow_natCast]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem ne_zero_iff_exists_coeff_ne_zero (f : MvPowerSeries σ R) :
    f ≠ 0 ↔ (∃ d : σ →₀ ℕ, coeff R d f ≠ 0)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
⊢ f ≠ 0 ↔ ∃ d, (coeff R d) f ≠ 0

Tactic:
simp only [MvPowerSeries.ext_iff, ne_eq, coeff_zero, not_forall]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem of_concat_eq_concat {as bs : List α} {a b : α} (h : as.concat a = bs.concat b) : as = bs ∧ a = b

Proof state:
α : Type u
as bs : List α
a b head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
h : head✝¹ = head✝ ∧ tail✝¹.concat a = tail✝.concat b
⊢ tail✝¹ = tail✝ ∧ a = b

Tactic:
apply of_concat_eq_concat h.2

Result:
no goals

Proof state:
α : Type u
as bs : List α
a b : α
h : as.concat a = bs.concat b
⊢ as = bs ∧ a = b

Tactic:
match as, bs with
| [], [] => simp [concat] at h; simp [h]
| [_], [] => simp [concat] at h
| _::_::_, [] => simp [concat] at h
| [], [_] => simp [concat] at h
| [], _::_::_ => simp [concat] at h
| _::_, _::_ => simp [concat] at h; simp [h]; apply of_concat_eq_concat h.2

Result:
no goals

Proof state:
α : Type u
as bs : List α
a b head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
h : head✝¹ = head✝ ∧ tail✝¹.concat a = tail✝.concat b
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝ ∧ a = b

Tactic:
simp [h]

Result:
α : Type u
as bs : List α
a b head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
h : head✝¹ = head✝ ∧ tail✝¹.concat a = tail✝.concat b
⊢ tail✝¹ = tail✝ ∧ a = b

Proof state:
α : Type u
as bs : List α
a b head✝¹ head✝ : α
tail✝ : List α
h : nil.concat a = (head✝¹ :: head✝ :: tail✝).concat b
⊢ nil = head✝¹ :: head✝ :: tail✝ ∧ a = b

Tactic:
simp [concat] at h

Result:
no goals

Proof state:
α : Type u
as bs : List α
a b head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
h : (head✝¹ :: tail✝¹).concat a = (head✝ :: tail✝).concat b
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝ ∧ a = b

Tactic:
simp [concat] at h

Result:
α : Type u
as bs : List α
a b head✝¹ : α
tail✝¹ : List α
head✝ : α
tail✝ : List α
h : head✝¹ = head✝ ∧ tail✝¹.concat a = tail✝.concat b
⊢ head✝¹ :: tail✝¹ = head✝ :: tail✝ ∧ a = b

Proof state:
α : Type u
as bs : List α
a b head✝¹ head✝ : α
tail✝ : List α
h : (head✝¹ :: head✝ :: tail✝).concat a = nil.concat b
⊢ head✝¹ :: head✝ :: tail✝ = nil ∧ a = b

Tactic:
simp [concat] at h

Result:
no goals

Proof state:
α : Type u
as bs : List α
a b : α
h : a = b
⊢ nil = nil ∧ a = b

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u
as bs : List α
a b : α
h : nil.concat a = nil.concat b
⊢ nil = nil ∧ a = b

Tactic:
simp [concat] at h

Result:
α : Type u
as bs : List α
a b : α
h : a = b
⊢ nil = nil ∧ a = b

Proof state:
α : Type u
as bs : List α
a b head✝ : α
h : (head✝ :: nil).concat a = nil.concat b
⊢ head✝ :: nil = nil ∧ a = b

Tactic:
simp [concat] at h

Result:
no goals

Proof state:
α : Type u
as bs : List α
a b head✝ : α
h : nil.concat a = (head✝ :: nil).concat b
⊢ nil = head✝ :: nil ∧ a = b

Tactic:
simp [concat] at h

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.swap_left_iff [NoZeroSMulDivisors R V] {x y z : P} (h : Wbtw R x y z) :
    Wbtw R y x z ↔ x = y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
x y z : P
h : Wbtw R x y z
⊢ Wbtw R y x z ↔ x = y

Tactic:
rw [← wbtw_swap_left_iff R z, and_iff_right h]

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Independence.lean
theorem dependent_pair_iff_eq (u v : ℙ K V) : Dependent ![u, v] ↔ u = v

Proof state:
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
⊢ ¬v.rep = 0 ∨ u = v

Tactic:
exact Or.inl (rep_nonzero v)

Result:
no goals

Proof state:
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
⊢ ¬(¬v.rep = 0 ∧ ∀ (a : K), a • v.rep ≠ (Projectivization.rep ∘ ![u, v]) 0) ↔ u = v

Tactic:
simp only [Matrix.cons_val_zero, not_and, not_forall, Classical.not_not, Function.comp_apply,
  ← mk_eq_mk_iff' K _ _ (rep_nonzero u) (rep_nonzero v), mk_rep, Classical.imp_iff_right_iff]

Result:
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
⊢ ¬v.rep = 0 ∨ u = v

Proof state:
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
⊢ Dependent ![u, v] ↔ u = v

Tactic:
rw [dependent_iff_not_independent, independent_iff, linearIndependent_fin2,
  Function.comp_apply, Matrix.cons_val_one, Matrix.head_cons, Ne]

Result:
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
⊢ ¬(¬v.rep = 0 ∧ ∀ (a : K), a • v.rep ≠ (Projectivization.rep ∘ ![u, v]) 0) ↔ u = v
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem changeForm_one : changeForm h (1 : CliffordAlgebra Q) = 1

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q Q' : QuadraticForm R M
B : BilinForm R M
h : BilinMap.toQuadraticMap B = Q' - Q
⊢ (changeForm h) 1 = 1

Tactic:
simpa using changeForm_algebraMap h (1 : R)

Result:
no goals
-- Mathlib/GroupTheory/PushoutI.lean
theorem summand_smul_def {i : ι} (g : G i) (w : NormalWord d) :
    of (φ := φ) i g • w = (equivPair i).symm
      { equivPair i w with
        head := g * (equivPair i w).head }

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
⊢ (of i) g • w =
    (equivPair i).symm
      (let __src := (equivPair i) w;
      { head := g * ((equivPair i) w).head, tail := __src.tail, fstIdx_ne := ⋯, normalized := ⋯ })

Tactic:
dsimp [NormalWord.mulAction, instHSMul, SMul.smul]

Result:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
⊢ (lift (fun x => MulAction.toEndHom) MulAction.toEndHom ⋯) ((of i) g) w =
    (equivPair i).symm
      { head := g * ((equivPair i) w).head, tail := ((equivPair i) w).tail, fstIdx_ne := ⋯, normalized := ⋯ }

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
⊢ MulAction.toEndHom g w =
    (equivPair i).symm
      { head := g * ((equivPair i) w).head, tail := ((equivPair i) w).tail, fstIdx_ne := ⋯, normalized := ⋯ }

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
⊢ (lift (fun x => MulAction.toEndHom) MulAction.toEndHom ⋯) ((of i) g) w =
    (equivPair i).symm
      { head := g * ((equivPair i) w).head, tail := ((equivPair i) w).tail, fstIdx_ne := ⋯, normalized := ⋯ }

Tactic:
rw [lift_of]

Result:
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
i : ι
g : G i
w : NormalWord d
⊢ MulAction.toEndHom g w =
    (equivPair i).symm
      { head := g * ((equivPair i) w).head, tail := ((equivPair i) w).tail, fstIdx_ne := ⋯, normalized := ⋯ }
-- Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean
@[to_additive le_sum_of_subadditive]
lemma le_prod_of_submultiplicative (f : α → β) (h_one : f 1 = 1)
    (h_mul : ∀ a b, f (a * b) ≤ f a * f b) (s : Multiset α) : f s.prod ≤ (s.map f).prod :=
  le_prod_of_submultiplicative_on_pred f (fun _ => True) h_one trivial (fun x y _ _ => h_mul x y)
    (by simp) s (by simp)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
h_one : f 1 = 1
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
⊢ ∀ (a b : α), (fun x => True) a → (fun x => True) b → (fun x => True) (a * b)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : OrderedCommMonoid β
f : α → β
h_one : f 1 = 1
h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b
s : Multiset α
⊢ ∀ a ∈ s, (fun x => True) a

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
theorem tendsto_integral_filter_of_dominated_convergence {ι} {l : Filter ι}
    [l.IsCountablyGenerated] {F : ι → ℝ → E} (bound : ℝ → ℝ)
    (hF_meas : ∀ᶠ n in l, AEStronglyMeasurable (F n) (μ.restrict (Ι a b)))
    (h_bound : ∀ᶠ n in l, ∀ᵐ x ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ bound x)
    (bound_integrable : IntervalIntegrable bound μ a b)
    (h_lim : ∀ᵐ x ∂μ, x ∈ Ι a b → Tendsto (fun n => F n x) l (𝓝 (f x))) :
    Tendsto (fun n => ∫ x in a..b, F n x ∂μ) l (𝓝 <| ∫ x in a..b, f x ∂μ)

Proof state:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ι : Type u_3
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → ℝ → E
bound : ℝ → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ bound x
bound_integrable : IntervalIntegrable bound μ a b
h_lim : ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → Tendsto (fun n => F n x) l (𝓝 (f x))
⊢ Tendsto (fun n => ∫ (x : ℝ) in a..b, F n x ∂μ) l (𝓝 (∫ (x : ℝ) in a..b, f x ∂μ))

Tactic:
simp only [intervalIntegrable_iff, intervalIntegral_eq_integral_uIoc,
  ← ae_restrict_iff' (α := ℝ) (μ := μ) measurableSet_uIoc] at *

Result:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ι : Type u_3
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → ℝ → E
bound : ℝ → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ‖F n x‖ ≤ bound x
bound_integrable : IntegrableOn bound (Ι a b) μ
h_lim : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), Tendsto (fun n => F n x) l (𝓝 (f x))
⊢ Tendsto (fun n => (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, F n x ∂μ) l
    (𝓝 ((if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ))

Proof state:
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
ι : Type u_3
l : Filter ι
inst✝ : l.IsCountablyGenerated
F : ι → ℝ → E
bound : ℝ → ℝ
hF_meas : ∀ᶠ (n : ι) in l, AEStronglyMeasurable (F n) (μ.restrict (Ι a b))
h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), ‖F n x‖ ≤ bound x
bound_integrable : IntegrableOn bound (Ι a b) μ
h_lim : ∀ᵐ (x : ℝ) ∂μ.restrict (Ι a b), Tendsto (fun n => F n x) l (𝓝 (f x))
⊢ Tendsto (fun n => (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, F n x ∂μ) l
    (𝓝 ((if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ))

Tactic:
exact tendsto_const_nhds.smul <|
  tendsto_integral_filter_of_dominated_convergence bound hF_meas h_bound bound_integrable h_lim

Result:
no goals