harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Dimension/StrongRankCondition.lean
theorem rank_eq_card_basis {ι : Type w} [Fintype ι] (h : Basis ι R M) :
    Module.rank R M = Fintype.card ι

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Fintype ι
h : Basis ι R M
⊢ Module.rank R M = ↑(Fintype.card ι)

Tactic:
classical
haveI := nontrivial_of_invariantBasisNumber R
rw [← h.mk_range_eq_rank, Cardinal.mk_fintype, Set.card_range_of_injective h.injective]

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Fintype ι
h : Basis ι R M
⊢ Module.rank R M = ↑(Fintype.card ι)

Tactic:
haveI := nontrivial_of_invariantBasisNumber R

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Fintype ι
h : Basis ι R M
this : Nontrivial R
⊢ Module.rank R M = ↑(Fintype.card ι)

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
inst✝ : Fintype ι
h : Basis ι R M
this : Nontrivial R
⊢ Module.rank R M = ↑(Fintype.card ι)

Tactic:
rw [← h.mk_range_eq_rank, Cardinal.mk_fintype, Set.card_range_of_injective h.injective]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem zipIdx_map_snd (m) (l : Vector α n) : map Prod.snd (zipIdx l m) = range' m n

Proof state:
case mk
α : Type u_1
m : Nat
l : Array α
⊢ map Prod.snd ({ toArray := l, size_toArray := ⋯ }.zipIdx m) = range' m l.size

Tactic:
simp [Array.zipIdx_map_snd]

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
l : Vector α n
⊢ map Prod.snd (l.zipIdx m) = range' m n

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
m : Nat
l : Array α
⊢ map Prod.snd ({ toArray := l, size_toArray := ⋯ }.zipIdx m) = range' m l.size
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Basic.lean
theorem ext_get? : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂
  | [], [], _ => rfl
  | _ :: _, [], h => nomatch h 0
  | [], _ :: _, h => nomatch h 0
  | a :: l₁, a' :: l₂, h => by
    have h0 : some a = some a' := h 0
    injection h0 with aa; simp only [aa, ext_get? fun n => h (n+1)]

Proof state:
α : Type u
a : α
l₁ : List α
a' : α
l₂ : List α
h : ∀ (n : Nat), (a :: l₁).get? n = (a' :: l₂).get? n
aa : a = a'
⊢ a :: l₁ = a' :: l₂

Tactic:
simp only [aa, ext_get? fun n => h (n+1)]

Result:
no goals

Proof state:
α : Type u
a : α
l₁ : List α
a' : α
l₂ : List α
h : ∀ (n : Nat), (a :: l₁).get? n = (a' :: l₂).get? n
⊢ a :: l₁ = a' :: l₂

Tactic:
have h0 : some a = some a' := h 0

Result:
α : Type u
a : α
l₁ : List α
a' : α
l₂ : List α
h : ∀ (n : Nat), (a :: l₁).get? n = (a' :: l₂).get? n
h0 : some a = some a'
⊢ a :: l₁ = a' :: l₂

Proof state:
α : Type u
a : α
l₁ : List α
a' : α
l₂ : List α
h : ∀ (n : Nat), (a :: l₁).get? n = (a' :: l₂).get? n
h0 : some a = some a'
⊢ a :: l₁ = a' :: l₂

Tactic:
injection h0 with aa

Result:
α : Type u
a : α
l₁ : List α
a' : α
l₂ : List α
h : ∀ (n : Nat), (a :: l₁).get? n = (a' :: l₂).get? n
aa : a = a'
⊢ a :: l₁ = a' :: l₂
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem cliqueFree_two : G.CliqueFree 2 ↔ G = ⊥

Proof state:
α : Type u_1
G : SimpleGraph α
h : G.CliqueFree 2
a b : α
hab : G.Adj a b
⊢ G.IsClique ↑{a, b}

Tactic:
simpa [hab.ne]

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 ↔ G = ⊥

Tactic:
constructor

Result:
case mp
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 → G = ⊥

case mpr
α : Type u_1
G : SimpleGraph α
⊢ G = ⊥ → G.CliqueFree 2

Proof state:
case mpr
α : Type u_1
G : SimpleGraph α
⊢ G = ⊥ → G.CliqueFree 2

Tactic:
rintro rfl

Result:
case mpr
α : Type u_1
⊢ ⊥.CliqueFree 2

Proof state:
case mp
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 → ∀ (x y : α), ¬G.Adj x y

Tactic:
exact fun h a b hab => h _ ⟨by simpa [hab.ne], card_pair hab.ne⟩

Result:
no goals

Proof state:
case mp
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 → G = ⊥

Tactic:
simp_rw [← edgeSet_eq_empty, Set.eq_empty_iff_forall_not_mem, Sym2.forall, mem_edgeSet]

Result:
case mp
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 2 → ∀ (x y : α), ¬G.Adj x y

Proof state:
case mpr
α : Type u_1
⊢ ⊥.CliqueFree 2

Tactic:
exact cliqueFree_bot le_rfl

Result:
no goals
-- Mathlib/Analysis/PSeries.lean
theorem sum_schlomilch_le' (hf : ∀ ⦃m n⦄, 1 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ n, 0 < u n)
    (hu : Monotone u) (n : ℕ) :
    (∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1))) ≤ ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k

Proof state:
case succ
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k
⊢ ∑ k ∈ range (n + 1), (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u (n + 1) + 1), f k

Tactic:
suffices (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k by
  rw [sum_range_succ, ← sum_Ico_consecutive]
  exacts [add_le_add ihn this,
    (add_le_add_right (hu n.zero_le) _ : u 0 + 1 ≤ u n + 1),
    add_le_add_right (hu n.le_succ) _]

Result:
case succ
M : Type u_1
inst✝ : OrderedAddCommMonoid M
f : ℕ → M
u : ℕ → ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
hu : Monotone u
n : ℕ
ihn : ∑ k ∈ range n, (u (k + 1) - u k) • f (u (k + 1)) ≤ ∑ k ∈ Ico (u 0 + 1) (u n + 1), f k
⊢ (u (n + 1) - u n) • f (u (n + 1)) ≤ ∑ k ∈ Ico (u n + 1) (u (n + 1) + 1), f k
-- Mathlib/Data/Matrix/Basis.lean
theorem matrix_eq_sum_stdBasisMatrix [AddCommMonoid α] [Fintype m] [Fintype n] (x : Matrix m n α) :
    x = ∑ i : m, ∑ j : n, stdBasisMatrix i j (x i j)

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ x i j = (∑ x_1 : m × n, stdBasisMatrix x_1.1 x_1.2 (x x_1.1 x_1.2)) i j

Tactic:
simp [stdBasisMatrix, Matrix.sum_apply, Matrix.of_apply, ← Prod.mk.inj_iff]

Result:
no goals

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ x i j = (∑ i : m, ∑ j : n, stdBasisMatrix i j (x i j)) i j

Tactic:
rw [← Fintype.sum_prod_type']

Result:
case a
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ x i j = (∑ x_1 : m × n, stdBasisMatrix x_1.1 x_1.2 (x x_1.1 x_1.2)) i j

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
⊢ x = ∑ i : m, ∑ j : n, stdBasisMatrix i j (x i j)

Tactic:
ext i j

Result:
case a
m : Type u_2
n : Type u_3
α : Type u_5
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ x i j = (∑ i : m, ∑ j : n, stdBasisMatrix i j (x i j)) i j
-- Mathlib/Algebra/Ring/NonZeroDivisors.lean
lemma dvd_cancel_left_mem_nonZeroDivisors (hr : r ∈ R⁰) : r * x ∣ r * y ↔ x ∣ y :=
  ⟨fun ⟨z, _⟩ ↦ ⟨z, by rwa [← mul_cancel_left_mem_nonZeroDivisors hr, ← mul_assoc]⟩,
    fun ⟨z, h⟩ ↦ ⟨z, by rw [h, ← mul_assoc]⟩⟩

Proof state:
R : Type u_1
inst✝ : CommRing R
r x y : R
hr : r ∈ R⁰
x✝ : r * x ∣ r * y
z : R
h✝ : r * y = r * x * z
⊢ y = x * z

Tactic:
rwa [← mul_cancel_left_mem_nonZeroDivisors hr, ← mul_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
r x y : R
hr : r ∈ R⁰
x✝ : x ∣ y
z : R
h : y = x * z
⊢ r * y = r * x * z

Tactic:
rw [h, ← mul_assoc]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem blocksFun_congr {n₁ n₂ : ℕ} (c₁ : Composition n₁) (c₂ : Composition n₂) (i₁ : Fin c₁.length)
    (i₂ : Fin c₂.length) (hn : n₁ = n₂) (hc : c₁.blocks = c₂.blocks) (hi : (i₁ : ℕ) = i₂) :
    c₁.blocksFun i₁ = c₂.blocksFun i₂

Proof state:
n₁ n₂ : ℕ
c₁ : Composition n₁
c₂ : Composition n₂
i₁ : Fin c₁.length
i₂ : Fin c₂.length
hn : n₁ = n₂
hc : c₁.blocks = c₂.blocks
hi : ↑i₁ = ↑i₂
⊢ c₁.blocksFun i₁ = c₂.blocksFun i₂

Tactic:
cases hn

Result:
case refl
n₁ : ℕ
c₁ : Composition n₁
i₁ : Fin c₁.length
c₂ : Composition n₁
i₂ : Fin c₂.length
hc : c₁.blocks = c₂.blocks
hi : ↑i₁ = ↑i₂
⊢ c₁.blocksFun i₁ = c₂.blocksFun i₂

Proof state:
case refl.refl
n₁ : ℕ
c₁ : Composition n₁
i₁ i₂ : Fin c₁.length
hi : ↑i₁ = ↑i₂
⊢ c₁.blocksFun i₁ = c₁.blocksFun i₂

Tactic:
congr

Result:
case refl.refl.e_a
n₁ : ℕ
c₁ : Composition n₁
i₁ i₂ : Fin c₁.length
hi : ↑i₁ = ↑i₂
⊢ i₁ = i₂

Proof state:
case refl
n₁ : ℕ
c₁ : Composition n₁
i₁ : Fin c₁.length
c₂ : Composition n₁
i₂ : Fin c₂.length
hc : c₁ = c₂
hi : ↑i₁ = ↑i₂
⊢ c₁.blocksFun i₁ = c₂.blocksFun i₂

Tactic:
cases hc

Result:
case refl.refl
n₁ : ℕ
c₁ : Composition n₁
i₁ i₂ : Fin c₁.length
hi : ↑i₁ = ↑i₂
⊢ c₁.blocksFun i₁ = c₁.blocksFun i₂

Proof state:
case refl
n₁ : ℕ
c₁ : Composition n₁
i₁ : Fin c₁.length
c₂ : Composition n₁
i₂ : Fin c₂.length
hc : c₁.blocks = c₂.blocks
hi : ↑i₁ = ↑i₂
⊢ c₁.blocksFun i₁ = c₂.blocksFun i₂

Tactic:
rw [← Composition.ext_iff] at hc

Result:
case refl
n₁ : ℕ
c₁ : Composition n₁
i₁ : Fin c₁.length
c₂ : Composition n₁
i₂ : Fin c₂.length
hc : c₁ = c₂
hi : ↑i₁ = ↑i₂
⊢ c₁.blocksFun i₁ = c₂.blocksFun i₂

Proof state:
case refl.refl.e_a
n₁ : ℕ
c₁ : Composition n₁
i₁ i₂ : Fin c₁.length
hi : ↑i₁ = ↑i₂
⊢ i₁ = i₂

Tactic:
rwa [Fin.ext_iff]

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Reduce.lean
theorem reduce_replicate (n : ℕ) (x : α × Bool) :
    reduce (.replicate n x) = .replicate n x

Proof state:
case succ.succ
α : Type u_1
inst✝ : DecidableEq α
x : α × Bool
n : ℕ
ih : reduce (List.replicate (n + 1) x) = List.replicate (n + 1) x
⊢ (List.casesOn (List.replicate (n + 1) x) [x] fun hd tl => if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate (n + 1) x

Tactic:
simp [List.replicate_succ]

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : DecidableEq α
x : α × Bool
n : ℕ
ih : reduce (List.replicate n x) = List.replicate n x
⊢ (List.casesOn (List.replicate n x) [x] fun hd tl => if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate n x

Tactic:
cases n with
| zero => simp
| succ n => simp [List.replicate_succ]

Result:
no goals

Proof state:
case succ.zero
α : Type u_1
inst✝ : DecidableEq α
x : α × Bool
ih : reduce (List.replicate 0 x) = List.replicate 0 x
⊢ (List.casesOn (List.replicate 0 x) [x] fun hd tl => if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate 0 x

Tactic:
simp

Result:
no goals

Proof state:
case zero
α : Type u_1
inst✝ : DecidableEq α
x : α × Bool
⊢ reduce (List.replicate 0 x) = List.replicate 0 x

Tactic:
simp [reduce]

Result:
no goals

Proof state:
case succ
α : Type u_1
inst✝ : DecidableEq α
x : α × Bool
n : ℕ
ih : reduce (List.replicate n x) = List.replicate n x
⊢ reduce (List.replicate (n + 1) x) = List.replicate (n + 1) x

Tactic:
rw [List.replicate_succ, reduce.cons, ih]

Result:
case succ
α : Type u_1
inst✝ : DecidableEq α
x : α × Bool
n : ℕ
ih : reduce (List.replicate n x) = List.replicate n x
⊢ (List.casesOn (List.replicate n x) [x] fun hd tl => if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate n x

Proof state:
α : Type u_1
inst✝ : DecidableEq α
n : ℕ
x : α × Bool
⊢ reduce (List.replicate n x) = List.replicate n x

Tactic:
induction n with
| zero => simp [reduce]
| succ n ih =>
  rw [List.replicate_succ, reduce.cons, ih]
  cases n with
  | zero => simp
  | succ n => simp [List.replicate_succ]

Result:
no goals
-- Mathlib/NumberTheory/DirichletCharacter/GaussSum.lean
/-- If `χ` is a primitive character, then the function `a ↦ gaussSum χ (e.mulShift a)`, for any
fixed additive character `e`, is a constant multiple of `χ⁻¹`. -/
lemma gaussSum_mulShift_of_isPrimitive [IsDomain R] {χ : DirichletCharacter R N}
    (hχ : IsPrimitive χ) (a : ZMod N) :
    gaussSum χ (e.mulShift a) = χ⁻¹ a * gaussSum χ e

Proof state:
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
⊢ gaussSum χ (e.mulShift a) = χ⁻¹ a * gaussSum χ e

Tactic:
by_cases ha : IsUnit a

Result:
case pos
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
ha : IsUnit a
⊢ gaussSum χ (e.mulShift a) = χ⁻¹ a * gaussSum χ e

case neg
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
ha : ¬IsUnit a
⊢ gaussSum χ (e.mulShift a) = χ⁻¹ a * gaussSum χ e

Proof state:
case pos
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
ha : IsUnit a
⊢ gaussSum χ (e.mulShift a) = χ⁻¹ a * (χ ↑ha.unit * gaussSum χ (e.mulShift ↑ha.unit))

Tactic:
rw [IsUnit.unit_spec, MulChar.inv_apply_eq_inv, Ring.inverse_mul_cancel_left _ _ (ha.map χ)]

Result:
no goals

Proof state:
case neg
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
ha : ¬IsUnit a
⊢ gaussSum χ (e.mulShift a) = χ⁻¹ a * gaussSum χ e

Tactic:
rw [MulChar.map_nonunit _ ha, zero_mul]

Result:
case neg
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
ha : ¬IsUnit a
⊢ gaussSum χ (e.mulShift a) = 0

Proof state:
case pos
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
ha : IsUnit a
⊢ gaussSum χ (e.mulShift a) = χ⁻¹ a * gaussSum χ e

Tactic:
conv_rhs => rw [← gaussSum_mulShift χ e ha.unit]

Result:
case pos
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
ha : IsUnit a
⊢ gaussSum χ (e.mulShift a) = χ⁻¹ a * (χ ↑ha.unit * gaussSum χ (e.mulShift ↑ha.unit))

Proof state:
case neg
N : ℕ
inst✝² : NeZero N
R : Type u_1
inst✝¹ : CommRing R
e : AddChar (ZMod N) R
inst✝ : IsDomain R
χ : DirichletCharacter R N
hχ : χ.IsPrimitive
a : ZMod N
ha : ¬IsUnit a
⊢ gaussSum χ (e.mulShift a) = 0

Tactic:
exact gaussSum_eq_zero_of_isPrimitive_of_not_isPrimitive _ hχ (not_isPrimitive_mulShift e ha)

Result:
no goals
-- Mathlib/Computability/RegularExpressions.lean
theorem mul_rmatch_iff (P Q : RegularExpression α) (x : List α) :
    (P * Q).rmatch x ↔ ∃ t u : List α, x = t ++ u ∧ P.rmatch t ∧ Q.rmatch u

Proof state:
case pos.mpr.intro.intro.intro.intro.nil.h
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
h : a :: x = [] ++ u
hP : P.rmatch [] = true
⊢ (Q.deriv a).rmatch x = true

Tactic:
rw [List.nil_append] at h

Result:
case pos.mpr.intro.intro.intro.intro.nil.h
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
h : a :: x = u
hP : P.rmatch [] = true
⊢ (Q.deriv a).rmatch x = true

Proof state:
case h.e'_2.h.e'_3.h.e'_4
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
u : List α
hQ : Q.rmatch u = true
b : α
t : List α
h : a = b ∧ x = t ++ u
hP : (P.deriv b).rmatch t = true
⊢ a = b

Tactic:
exact h.1

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
⊢ (if P.matchEpsilon = true then P.deriv a * Q + Q.deriv a else P.deriv a * Q).rmatch x = true ↔
    ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

Tactic:
split_ifs with hepsilon

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : P.matchEpsilon = true
⊢ (P.deriv a * Q + Q.deriv a).rmatch x = true ↔ ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
x : List α
ih : ∀ (P Q : RegularExpression α), (P * Q).rmatch x = true ↔ ∃ t u, x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
P Q : RegularExpression α
hepsilon : ¬P.matchEpsilon = true
⊢ (P.deriv a * Q).rmatch x = true ↔ ∃ t u, a :: x = t ++ u ∧ P.rmatch t = true ∧ Q.rmatch u = true
-- Mathlib/MeasureTheory/Integral/TorusIntegral.lean
theorem torusIntegral_add (hf : TorusIntegrable f c R) (hg : TorusIntegrable g c R) :
    (∯ x in T(c, R), f x + g x) = (∯ x in T(c, R), f x) + ∯ x in T(c, R), g x

Proof state:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : (Fin n → ℂ) → E
c : Fin n → ℂ
R : Fin n → ℝ
hf : TorusIntegrable f c R
hg : TorusIntegrable g c R
⊢ (∯ (x : Fin n → ℂ) in T(c, R), f x + g x) = (∯ (x : Fin n → ℂ) in T(c, R), f x) + ∯ (x : Fin n → ℂ) in T(c, R), g x

Tactic:
simpa only [torusIntegral, smul_add, Pi.add_apply] using
  integral_add hf.function_integrable hg.function_integrable

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
theorem log_of_nat_eq_posLog {n : ℕ} : log⁺ n = log n

Proof state:
case pos
n : ℕ
hn : n = 0
⊢ log⁺ ↑n = log ↑n

Tactic:
simp [hn, posLog]

Result:
no goals

Proof state:
n : ℕ
⊢ log⁺ ↑n = log ↑n

Tactic:
by_cases hn : n = 0

Result:
case pos
n : ℕ
hn : n = 0
⊢ log⁺ ↑n = log ↑n

case neg
n : ℕ
hn : ¬n = 0
⊢ log⁺ ↑n = log ↑n

Proof state:
case neg
n : ℕ
hn : ¬n = 0
⊢ log⁺ ↑n = log ↑n

Tactic:
simp [posLog_eq_log, Nat.one_le_iff_ne_zero.2 hn]

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
lemma sum_apply_eq_ite [Fintype α] [DecidableEq α] (a : α) :
    ∑ ψ : AddChar α ℂ, ψ a = if a = 0 then (Fintype.card α : ℂ) else 0

Proof state:
α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
a : α
⊢ ∑ ψ : AddChar α ℂ, ψ a = if a = 0 then ↑(Fintype.card α) else 0

Tactic:
simpa using sum_eq_ite (doubleDualEmb a : AddChar (AddChar α ℂ) ℂ)

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem mem_of_closed' {s : Set α} (hs : IsClosed s) {a : α} :
    a ∈ s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
hs : IsClosed s
a : α
⊢ a ∈ s ↔ ∀ ε > 0, ∃ b ∈ s, dist a b < ε

Tactic:
simpa only [hs.closure_eq] using @mem_closure_iff _ _ s a

Result:
no goals
-- Mathlib/Analysis/MeanInequalitiesPow.lean
theorem rpow_add_rpow_le {p q : ℝ} (a b : ℝ≥0) (hp_pos : 0 < p) (hpq : p ≤ q) :
    (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Proof state:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p

Tactic:
rwa [one_div_div] at h_rpow_add_rpow_le_add

Result:
no goals

Proof state:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p

Tactic:
refine rpow_add_rpow_le_add (a ^ p) (b ^ p) ?_

Result:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
⊢ 1 ≤ q / p

Proof state:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Tactic:
rw [h_rpow a, h_rpow b, one_div p, NNReal.le_rpow_inv_iff hp_pos, ← NNReal.rpow_mul, mul_comm,
  mul_one_div]

Result:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p

Proof state:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Tactic:
have h_rpow_add_rpow_le_add :
  ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p := by
  refine rpow_add_rpow_le_add (a ^ p) (b ^ p) ?_
  rwa [one_le_div hp_pos]

Result:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Proof state:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
⊢ 1 ≤ q / p

Tactic:
rwa [one_le_div hp_pos]

Result:
no goals

Proof state:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Tactic:
have h_rpow : ∀ a : ℝ≥0, a ^ q = (a ^ p) ^ (q / p) := fun a => by
  rw [← NNReal.rpow_mul, div_eq_inv_mul, ← mul_assoc, mul_inv_cancel₀ hp_pos.ne.symm,
    one_mul]

Result:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)

Proof state:
p q : ℝ
a✝ b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0
⊢ a ^ q = (a ^ p) ^ (q / p)

Tactic:
rw [← NNReal.rpow_mul, div_eq_inv_mul, ← mul_assoc, mul_inv_cancel₀ hp_pos.ne.symm,
  one_mul]

Result:
no goals
-- Mathlib/Algebra/Order/Rearrangement.lean
theorem AntivaryOn.sum_smul_lt_sum_smul_comp_perm_iff (hfg : AntivaryOn f g s)
    (hσ : {x | σ x ≠ x} ⊆ s) :
    ∑ i ∈ s, f i • g i < ∑ i ∈ s, f i • g (σ i) ↔ ¬AntivaryOn f (g ∘ σ) s

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝⁴ : LinearOrderedSemiring α
inst✝³ : ExistsAddOfLE α
inst✝² : LinearOrderedCancelAddCommMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
s : Finset ι
σ : Perm ι
f : ι → α
g : ι → β
hfg : AntivaryOn f g ↑s
hσ : {x | σ x ≠ x} ⊆ ↑s
⊢ ∑ i ∈ s, f i • g i < ∑ i ∈ s, f i • g (σ i) ↔ ¬AntivaryOn f (g ∘ ⇑σ) ↑s

Tactic:
simp [← hfg.sum_smul_comp_perm_eq_sum_smul_iff hσ, lt_iff_le_and_ne, eq_comm,
  hfg.sum_smul_le_sum_smul_comp_perm hσ]

Result:
no goals