harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/MeanInequalities.lean
theorem inner_le_Lp_mul_Lq (hpq : IsConjExponent p q) :
    ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) * (∑ i ∈ s, |g i| ^ q) ^ (1 / q)

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.IsConjExponent q
this : ∑ x ∈ s, |f x| * |g x| ≤ (∑ x ∈ s, |f x| ^ p) ^ (1 / p) * (∑ x ∈ s, |g x| ^ q) ^ (1 / q)
i : ι
x✝ : i ∈ s
⊢ f i * g i ≤ |f i| * |g i|

Tactic:
simp only [← abs_mul, le_abs_self]

Result:
no goals

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.IsConjExponent q
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) * (∑ i ∈ s, |g i| ^ q) ^ (1 / q)

Tactic:
have :=
  NNReal.coe_le_coe.2
    (NNReal.inner_le_Lp_mul_Lq s (fun i => ⟨_, abs_nonneg (f i)⟩) (fun i => ⟨_, abs_nonneg (g i)⟩)
      hpq)

Result:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.IsConjExponent q
this :
  ↑(∑ i ∈ s, (fun i => ⟨|f i|, ⋯⟩) i * (fun i => ⟨|g i|, ⋯⟩) i) ≤
    ↑((∑ i ∈ s, (fun i => ⟨|f i|, ⋯⟩) i ^ p) ^ (1 / p) * (∑ i ∈ s, (fun i => ⟨|g i|, ⋯⟩) i ^ q) ^ (1 / q))
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) * (∑ i ∈ s, |g i| ^ q) ^ (1 / q)

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.IsConjExponent q
this :
  ↑(∑ i ∈ s, (fun i => ⟨|f i|, ⋯⟩) i * (fun i => ⟨|g i|, ⋯⟩) i) ≤
    ↑((∑ i ∈ s, (fun i => ⟨|f i|, ⋯⟩) i ^ p) ^ (1 / p) * (∑ i ∈ s, (fun i => ⟨|g i|, ⋯⟩) i ^ q) ^ (1 / q))
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) * (∑ i ∈ s, |g i| ^ q) ^ (1 / q)

Tactic:
push_cast at this

Result:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.IsConjExponent q
this : ∑ x ∈ s, |f x| * |g x| ≤ (∑ x ∈ s, |f x| ^ p) ^ (1 / p) * (∑ x ∈ s, |g x| ^ q) ^ (1 / q)
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) * (∑ i ∈ s, |g i| ^ q) ^ (1 / q)

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.IsConjExponent q
this : ∑ x ∈ s, |f x| * |g x| ≤ (∑ x ∈ s, |f x| ^ p) ^ (1 / p) * (∑ x ∈ s, |g x| ^ q) ^ (1 / q)
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, |f i| ^ p) ^ (1 / p) * (∑ i ∈ s, |g i| ^ q) ^ (1 / q)

Tactic:
refine le_trans (sum_le_sum fun i _ => ?_) this

Result:
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : p.IsConjExponent q
this : ∑ x ∈ s, |f x| * |g x| ≤ (∑ x ∈ s, |f x| ^ p) ^ (1 / p) * (∑ x ∈ s, |g x| ^ q) ^ (1 / q)
i : ι
x✝ : i ∈ s
⊢ f i * g i ≤ |f i| * |g i|
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_empty : (#[] : Array (Array α)).flatten = #[]

Proof state:
α : Type u_1
⊢ #[] = #[]

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
⊢ #[].flatten = #[]

Tactic:
simp [flatten]

Result:
α : Type u_1
⊢ #[] = #[]
-- Mathlib/Order/Filter/Basic.lean
theorem eventually_iff_all_subsets {f : Filter α} {p : α → Prop} :
    (∀ᶠ x in f, p x) ↔ ∀ (s : Set α), ∀ᶠ x in f, x ∈ s → p x where
  mp h _

Proof state:
α : Type u
f : Filter α
p : α → Prop
h : ∀ (s : Set α), ∀ᶠ (x : α) in f, x ∈ s → p x
⊢ ∀ᶠ (x : α) in f, p x

Tactic:
filter_upwards [h univ] with _ pa using pa (by simp)

Result:
no goals

Proof state:
α : Type u
f : Filter α
p : α → Prop
h : ∀ᶠ (x : α) in f, p x
x✝ : Set α
⊢ ∀ᶠ (x : α) in f, x ∈ x✝ → p x

Tactic:
filter_upwards [h] with _ pa _ using pa

Result:
no goals

Proof state:
α : Type u
f : Filter α
p : α → Prop
h : ∀ (s : Set α), ∀ᶠ (x : α) in f, x ∈ s → p x
a✝ : α
pa : a✝ ∈ univ → p a✝
⊢ a✝ ∈ univ

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_congr_ae {f g : α → G} (h : f =ᵐ[μ] g) : ∫ a, f a ∂μ = ∫ a, g a ∂μ

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
h : f =ᶠ[ae μ] g
hG : CompleteSpace G
⊢ ∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ

Tactic:
simp only [integral, hG, L1.integral]

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
h : f =ᶠ[ae μ] g
hG : CompleteSpace G
⊢ (if h : True then if hf : Integrable (fun a => f a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
    else 0) =
    if h : True then if hf : Integrable (fun a => g a) μ then L1.integralCLM (Integrable.toL1 (fun a => g a) hf) else 0
    else 0

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
h : f =ᶠ[ae μ] g
hG : CompleteSpace G
⊢ (if h : True then if hf : Integrable (fun a => f a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
    else 0) =
    if h : True then if hf : Integrable (fun a => g a) μ then L1.integralCLM (Integrable.toL1 (fun a => g a) hf) else 0
    else 0

Tactic:
exact setToFun_congr_ae (dominatedFinMeasAdditive_weightedSMul μ) h

Result:
no goals

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
h : f =ᶠ[ae μ] g
hG : ¬CompleteSpace G
⊢ ∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ

Tactic:
simp [integral, hG]

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
h : f =ᶠ[ae μ] g
⊢ ∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ

Tactic:
by_cases hG : CompleteSpace G

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
h : f =ᶠ[ae μ] g
hG : CompleteSpace G
⊢ ∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ

case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f g : α → G
h : f =ᶠ[ae μ] g
hG : ¬CompleteSpace G
⊢ ∫ (a : α), f a ∂μ = ∫ (a : α), g a ∂μ
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
lemma Matrix.linearIndependent_cols_of_isUnit {R : Type*} [CommRing R] [Fintype m]
    {A : Matrix m m R} [DecidableEq m] (ha : IsUnit A) :
    LinearIndependent R (fun i ↦ A.transpose i)

Proof state:
m : Type u_4
R : Type u_6
inst✝² : CommRing R
inst✝¹ : Fintype m
A : Matrix m m R
inst✝ : DecidableEq m
ha : IsUnit A
⊢ Function.Injective A.mulVec

Tactic:
exact Matrix.mulVec_injective_of_isUnit ha

Result:
no goals

Proof state:
m : Type u_4
R : Type u_6
inst✝² : CommRing R
inst✝¹ : Fintype m
A : Matrix m m R
inst✝ : DecidableEq m
ha : IsUnit A
⊢ LinearIndependent R fun i => Aᵀ i

Tactic:
rw [← Matrix.mulVec_injective_iff]

Result:
m : Type u_4
R : Type u_6
inst✝² : CommRing R
inst✝¹ : Fintype m
A : Matrix m m R
inst✝ : DecidableEq m
ha : IsUnit A
⊢ Function.Injective A.mulVec
-- Mathlib/Computability/RegularExpressions.lean
theorem matches'_map (f : α → β) :
    ∀ P : RegularExpression α, (P.map f).matches' = Language.map f P.matches'
  | 0 => (map_zero _).symm
  | 1 => (map_one _).symm
  | char a => by
    rw [eq_comm]
    exact image_singleton
  | R + S => by simp only [matches'_map, map, matches'_add, map_add]
  | R * S => by simp [matches'_map]
  | star R => by simp [matches'_map]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
R S : RegularExpression α
⊢ (map f (R * S)).matches' = (Language.map f) (R * S).matches'

Tactic:
simp [matches'_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ (map f (char a)).matches' = (Language.map f) (char a).matches'

Tactic:
rw [eq_comm]

Result:
α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ (Language.map f) (char a).matches' = (map f (char a)).matches'

Proof state:
α : Type u_1
β : Type u_2
f : α → β
R : RegularExpression α
⊢ (map f R.star).matches' = (Language.map f) R.star.matches'

Tactic:
simp [matches'_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
R S : RegularExpression α
⊢ (map f (R + S)).matches' = (Language.map f) (R + S).matches'

Tactic:
simp only [matches'_map, map, matches'_add, map_add]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ (Language.map f) (char a).matches' = (map f (char a)).matches'

Tactic:
exact image_singleton

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem image_fst_graph [DecidableEq α] (f : α →₀ M) : f.graph.image Prod.fst = f.support

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ image Prod.fst f.graph = f.support

Tactic:
simp only [graph, map_eq_image, image_image, Embedding.coeFn_mk, Function.comp_def, image_id']

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ image Prod.fst f.graph = f.support

Tactic:
classical
simp only [graph, map_eq_image, image_image, Embedding.coeFn_mk, Function.comp_def, image_id']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem countP_attach (l : Array α) (p : α → Bool) :
    l.attach.countP (fun a : {x // x ∈ l} => p a) = l.countP p

Proof state:
α : Type u_1
l : Array α
p : α → Bool
⊢ countP (fun a => p a.val) l.attach = countP p l

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ countP (fun a => p a.val) { toList := toList✝ }.attach = countP p { toList := toList✝ }

Proof state:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ countP (fun a => p a.val) { toList := toList✝ }.attach = countP p { toList := toList✝ }

Tactic:
simp [Function.comp_def]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/FiniteDimension.lean
theorem LinearIndependent.eventually {ι} [Finite ι] {f : ι → E}
    (hf : LinearIndependent 𝕜 f) : ∀ᶠ g in 𝓝 f, LinearIndependent 𝕜 g

Proof state:
case intro.intro.intro.h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : CompleteSpace 𝕜
ι : Type u_1
inst✝ : Finite ι
f : ι → E
val✝ : Fintype ι
hf : LinearMap.ker ((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i)) = ⊥
K : ℝ≥0
K0 : K > 0
hK : AntilipschitzWith K ⇑((LinearMap.lsum 𝕜 (fun x => 𝕜) ℕ) fun i => LinearMap.id.smulRight (f i))
this : Tendsto (fun g => ∑ i : ι, ‖g i - f i‖) (𝓝 f) (𝓝 0)
g : ι → E
hg : ∑ i : ι, ‖g i - f i‖₊ < K⁻¹
v u : ι → 𝕜
i : ι
x✝ : i ∈ Finset.univ
⊢ ‖v i - u i‖ ≤ ‖v - u‖

Tactic:
exact norm_le_pi_norm (v - u) i

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
@[to_additive]
protected lemma IsOfFinOrder.orderOf_pow (h : IsOfFinOrder x) :
    orderOf (x ^ n) = orderOf x / gcd (orderOf x) n

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : IsOfFinOrder x
⊢ minimalPeriod (fun x_1 => x ^ n * x_1) 1 =
    minimalPeriod (fun x_1 => x * x_1) 1 / (minimalPeriod (fun x_1 => x * x_1) 1).gcd n

Tactic:
rw [← minimalPeriod_iterate_eq_div_gcd' h, mul_left_iterate]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : IsOfFinOrder x
⊢ orderOf (x ^ n) = orderOf x / (orderOf x).gcd n

Tactic:
unfold orderOf

Result:
G : Type u_1
inst✝ : Monoid G
x : G
n : ℕ
h : IsOfFinOrder x
⊢ minimalPeriod (fun x_1 => x ^ n * x_1) 1 =
    minimalPeriod (fun x_1 => x * x_1) 1 / (minimalPeriod (fun x_1 => x * x_1) 1).gcd n
-- Mathlib/.lake/packages/batteries/Batteries/Lean/EStateM.lean
theorem map_eq_ok {ε σ α β} {f : α → β} {x : Result ε σ α} {b : β} {s : σ} :
    x.map f = .ok b s ↔ ∃ a, x = .ok a s ∧ b = f a

Proof state:
ε σ α β : Type u_1
f : α → β
x : Result ε σ α
b : β
s : σ
⊢ map f x = ok b s ↔ ∃ a, x = ok a s ∧ b = f a

Tactic:
cases x <;> simp [and_assoc, and_comm, eq_comm]

Result:
no goals
-- Mathlib/Algebra/Module/Projective.lean
theorem Projective.of_basis {ι : Type*} (b : Basis ι R P) : Projective R P

Proof state:
R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_8
b : Basis ι R P
⊢ Projective R P

Tactic:
use b.constr ℕ fun i => Finsupp.single (b i) (1 : R)

Result:
case h
R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_8
b : Basis ι R P
⊢ Function.LeftInverse ⇑(linearCombination R id) ⇑((b.constr ℕ) fun i => Finsupp.single (b i) 1)

Proof state:
case h
R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_8
b : Basis ι R P
⊢ Function.LeftInverse ⇑(linearCombination R id) ⇑((b.constr ℕ) fun i => Finsupp.single (b i) 1)

Tactic:
intro m

Result:
case h
R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_8
b : Basis ι R P
m : P
⊢ (linearCombination R id) (((b.constr ℕ) fun i => Finsupp.single (b i) 1) m) = m

Proof state:
case h
R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_8
b : Basis ι R P
m : P
⊢ ((b.repr m).sum fun a b_1 => b_1 • b a) = m

Tactic:
exact b.linearCombination_repr m

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_8
b : Basis ι R P
m : P
⊢ (linearCombination R id) (((b.constr ℕ) fun i => Finsupp.single (b i) 1) m) = m

Tactic:
simp only [b.constr_apply, mul_one, id, Finsupp.smul_single', Finsupp.linearCombination_single,
  map_finsupp_sum]

Result:
case h
R : Type u_1
inst✝² : Semiring R
P : Type u_2
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
ι : Type u_8
b : Basis ι R P
m : P
⊢ ((b.repr m).sum fun a b_1 => b_1 • b a) = m
-- Mathlib/Algebra/Lie/OfAssociative.lean
lemma LieModule.toEnd_lie (x y : L) (z : M) :
    (φ x) ⁅y, z⁆ = ⁅ad R L x y, z⁆ + ⁅y, φ x z⁆

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
x y : L
z : M
⊢ (φ x) ⁅y, z⁆ = ⁅((ad R L) x) y, z⁆ + ⁅y, (φ x) z⁆

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem exists_ne_one_of_finprod_mem_ne_one (h : ∏ᶠ i ∈ s, f i ≠ 1) : ∃ x ∈ s, f x ≠ 1

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
h : ∏ᶠ (i : α) (_ : i ∈ s), f i ≠ 1
h' : ∀ x ∈ s, f x = 1
⊢ False

Tactic:
exact h (finprod_mem_of_eqOn_one h')

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
h : ∏ᶠ (i : α) (_ : i ∈ s), f i ≠ 1
⊢ ∃ x ∈ s, f x ≠ 1

Tactic:
by_contra! h'

Result:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
s : Set α
h : ∏ᶠ (i : α) (_ : i ∈ s), f i ≠ 1
h' : ∀ x ∈ s, f x = 1
⊢ False
-- Mathlib/LinearAlgebra/PerfectPairing/Basic.lean
@[simp]
lemma dualAnnihilator_map_linearEquiv_flip_symm (p : Submodule R (Dual R N)) :
    (p.map e.flip.symm).dualAnnihilator = p.dualCoannihilator.map e

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R (Dual R N)
this : IsReflexive R N
⊢ (map e.flip.symm p).dualAnnihilator = map e p.dualCoannihilator

Tactic:
rw [← map_dualCoannihilator_linearEquiv_flip, flip_flip]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R (Dual R N)
⊢ (map e.flip.symm p).dualAnnihilator = map e p.dualCoannihilator

Tactic:
have : IsReflexive R N := e.isReflexive_of_equiv_dual_of_isReflexive

Result:
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsReflexive R M
e : N ≃ₗ[R] Dual R M
p : Submodule R (Dual R N)
this : IsReflexive R N
⊢ (map e.flip.symm p).dualAnnihilator = map e p.dualCoannihilator
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Erase.lean
theorem getElem?_eraseIdx_of_lt (l : Vector α n) (i : Nat) (h : i < n) (j : Nat) (h' : j < i) :
    (l.eraseIdx i)[j]? = l[j]?

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
j : Nat
h' : j < i
⊢ (if j < i then l[j]? else l[j + 1]?) = l[j]?

Tactic:
simp [h']

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
j : Nat
h' : j < i
⊢ (l.eraseIdx i h)[j]? = l[j]?

Tactic:
rw [getElem?_eraseIdx]

Result:
α : Type u_1
n : Nat
l : Vector α n
i : Nat
h : i < n
j : Nat
h' : j < i
⊢ (if j < i then l[j]? else l[j + 1]?) = l[j]?
-- Mathlib/Data/Rat/Defs.lean
theorem coe_int_num_of_den_eq_one {q : ℚ} (hq : q.den = 1) : (q.num : ℚ) = q

Proof state:
q : ℚ
hq : q.den = 1
⊢ ↑q.num = q

Tactic:
conv_rhs => rw [← num_divInt_den q, hq]

Result:
q : ℚ
hq : q.den = 1
⊢ ↑q.num = q.num /. ↑1

Proof state:
q : ℚ
hq : q.den = 1
⊢ ↑q.num = q.num /. ↑1

Tactic:
rw [intCast_eq_divInt]

Result:
q : ℚ
hq : q.den = 1
⊢ q.num /. 1 = q.num /. ↑1

Proof state:
q : ℚ
hq : q.den = 1
⊢ q.num /. 1 = q.num /. ↑1

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Norm.lean
theorem absNorm_div_norm_eq_absNorm_div_norm {I : FractionalIdeal R⁰ K} (a : R⁰) (I₀ : Ideal R)
    (h : a • (I : Submodule R K) = Submodule.map (Algebra.linearMap R K) I₀) :
    (Ideal.absNorm I.num : ℚ) / |Algebra.norm ℤ (I.den : R)| =
      (Ideal.absNorm I₀ : ℚ) / |Algebra.norm ℤ (a : R)|

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Module.Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀
⊢ ↑(Ideal.absNorm I.num) / ↑|(Algebra.norm ℤ) ↑I.den| = ↑(Ideal.absNorm I₀) / ↑|(Algebra.norm ℤ) ↑a|

Tactic:
rw [div_eq_div_iff]

Result:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Module.Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀
⊢ ↑(Ideal.absNorm I.num) * ↑|(Algebra.norm ℤ) ↑a| = ↑(Ideal.absNorm I₀) * ↑|(Algebra.norm ℤ) ↑I.den|

case hb
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Module.Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀
⊢ ↑|(Algebra.norm ℤ) ↑I.den| ≠ 0

case hd
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Module.Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀
⊢ ↑|(Algebra.norm ℤ) ↑a| ≠ 0

Proof state:
case hb
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Module.Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀
⊢ ↑|(Algebra.norm ℤ) ↑I.den| ≠ 0

case hd
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Module.Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • ↑I = Submodule.map (Algebra.linearMap R K) I₀
⊢ ↑|(Algebra.norm ℤ) ↑a| ≠ 0

Tactic:
all_goals simp [Algebra.norm_eq_zero_iff]

Result:
no goals
-- Mathlib/Algebra/Lie/InvariantForm.lean
lemma mem_orthogonal (N : LieSubmodule R L M) (y : M) :
    y ∈ orthogonal Φ hΦ_inv N ↔ ∀ x ∈ N, Φ x y = 0

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
Φ : LinearMap.BilinForm R M
hΦ_inv : LinearMap.BilinForm.lieInvariant L Φ
N : LieSubmodule R L M
y : M
⊢ y ∈ orthogonal Φ hΦ_inv N ↔ ∀ x ∈ N, (Φ x) y = 0

Tactic:
simp [orthogonal, LinearMap.BilinForm.isOrtho_def, LinearMap.BilinForm.mem_orthogonal_iff]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Construction.lean
@[reassoc (attr := simp)]
lemma functorMapSrc_functorObjTop :
    functorMapSrc f τ ≫ functorObjTop f πY = functorObjTop f πX ≫ τ.left

Proof state:
case h.mk
C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } ≫ functorMapSrc f τ ≫ functorObjTop f πY =
    Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } ≫ functorObjTop f πX ≫ τ.left

Tactic:
simp [ι_functorMapSrc_assoc f τ i t b w _ rfl]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
⊢ functorMapSrc f τ ≫ functorObjTop f πY = functorObjTop f πX ≫ τ.left

Tactic:
ext ⟨i, t, b, w⟩

Result:
case h.mk
C : Type u
inst✝² : Category.{v, u} C
I : Type w
A B : I → C
f : (i : I) → A i ⟶ B i
S T X Y : C
πX : X ⟶ S
πY : Y ⟶ T
τ : Arrow.mk πX ⟶ Arrow.mk πY
inst✝¹ : HasColimitsOfShape (Discrete (FunctorObjIndex f πX)) C
inst✝ : HasColimitsOfShape (Discrete (FunctorObjIndex f πY)) C
i : I
t : A i ⟶ X
b : B i ⟶ S
w : t ≫ πX = f i ≫ b
⊢ Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } ≫ functorMapSrc f τ ≫ functorObjTop f πY =
    Sigma.ι (functorObjSrcFamily f πX) { i := i, t := t, b := b, w := w } ≫ functorObjTop f πX ≫ τ.left
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem typein_apply {α β} {r : α → α → Prop} {s : β → β → Prop} [IsWellOrder α r] [IsWellOrder β s]
    (f : r ≼i s) (a : α) : typein s (f a) = typein r a

Proof state:
α β : Type u_1
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≼i s
a : α
⊢ (typein s).toRelEmbedding (f a) = (typein r).toRelEmbedding a

Tactic:
rw [← f.transPrincipal_apply _ a, (f.transPrincipal _).eq]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
theorem inv (h : IsPrimitiveRoot ζ k) : IsPrimitiveRoot ζ⁻¹ k :=
  { pow_eq_one

Proof state:
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
hl : ζ⁻¹ ^ l = 1
⊢ k ∣ l

Tactic:
apply h.dvd_of_pow_eq_one l

Result:
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
hl : ζ⁻¹ ^ l = 1
⊢ ζ ^ l = 1

Proof state:
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
⊢ ζ⁻¹ ^ k = 1

Tactic:
simp only [h.pow_eq_one, inv_one, eq_self_iff_true, inv_pow]

Result:
no goals

Proof state:
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
⊢ ∀ (l : ℕ), ζ⁻¹ ^ l = 1 → k ∣ l

Tactic:
intro l hl

Result:
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
hl : ζ⁻¹ ^ l = 1
⊢ k ∣ l

Proof state:
G : Type u_3
inst✝ : DivisionCommMonoid G
k : ℕ
ζ : G
h : IsPrimitiveRoot ζ k
l : ℕ
hl : ζ⁻¹ ^ l = 1
⊢ ζ ^ l = 1

Tactic:
rw [← inv_inj, ← inv_pow, hl, inv_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem cons_lt_cons_iff [LT α] {a b} {l₁ l₂ : List α} :
    (a :: l₁) < (b :: l₂) ↔ a < b ∨ a = b ∧ l₁ < l₂

Proof state:
α : Type u_1
inst✝ : LT α
a b : α
l₁ l₂ : List α
⊢ a :: l₁ < b :: l₂ ↔ a < b ∨ a = b ∧ l₁ < l₂

Tactic:
dsimp only [instLT, List.lt]

Result:
α : Type u_1
inst✝ : LT α
a b : α
l₁ l₂ : List α
⊢ Lex (fun x1 x2 => x1 < x2) (a :: l₁) (b :: l₂) ↔ a < b ∨ a = b ∧ Lex (fun x1 x2 => x1 < x2) l₁ l₂

Proof state:
α : Type u_1
inst✝ : LT α
a b : α
l₁ l₂ : List α
⊢ Lex (fun x1 x2 => x1 < x2) (a :: l₁) (b :: l₂) ↔ a < b ∨ a = b ∧ Lex (fun x1 x2 => x1 < x2) l₁ l₂

Tactic:
simp [cons_lex_cons_iff]

Result:
no goals