harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem mul_div_lipschitzWith (hf : AntilipschitzWith Kf f) (hg : LipschitzWith Kg (g / f))
    (hK : Kg < Kf⁻¹) : AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g

Proof state:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
hf : AntilipschitzWith Kf f
hg : LipschitzWith Kg (g / f)
hK : Kg < Kf⁻¹
⊢ AntilipschitzWith (Kf⁻¹ - Kg)⁻¹ g

Tactic:
simpa only [Pi.div_apply, mul_div_cancel] using hf.mul_lipschitzWith hg hK

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma HasUnifEigenvalue.pow {f : End R M} {μ : R} (h : f.HasUnifEigenvalue μ 1) (n : ℕ) :
    (f ^ n).HasUnifEigenvalue (μ ^ n) 1

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
h : f.HasUnifEigenvalue μ 1
n : ℕ
⊢ (f ^ n).HasUnifEigenvalue (μ ^ n) 1

Tactic:
rw [HasUnifEigenvalue, Submodule.ne_bot_iff]

Result:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
h : f.HasUnifEigenvalue μ 1
n : ℕ
⊢ ∃ x ∈ ((f ^ n).genEigenspace (μ ^ n)) 1, x ≠ 0

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
h : f.HasUnifEigenvalue μ 1
n : ℕ
m : M
hm : f.HasUnifEigenvector μ 1 m
⊢ m ∈ ((f ^ n).genEigenspace (μ ^ n)) 1

Tactic:
simpa [mem_genEigenspace_one] using hm.pow_apply n

Result:
no goals

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
h : f.HasUnifEigenvalue μ 1
n : ℕ
⊢ ∃ x ∈ ((f ^ n).genEigenspace (μ ^ n)) 1, x ≠ 0

Tactic:
obtain ⟨m : M, hm⟩ := h.exists_hasUnifEigenvector

Result:
case intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
h : f.HasUnifEigenvalue μ 1
n : ℕ
m : M
hm : f.HasUnifEigenvector μ 1 m
⊢ ∃ x ∈ ((f ^ n).genEigenspace (μ ^ n)) 1, x ≠ 0

Proof state:
case intro
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
h : f.HasUnifEigenvalue μ 1
n : ℕ
m : M
hm : f.HasUnifEigenvector μ 1 m
⊢ ∃ x ∈ ((f ^ n).genEigenspace (μ ^ n)) 1, x ≠ 0

Tactic:
exact ⟨m, by simpa [mem_genEigenspace_one] using hm.pow_apply n, hm.2⟩

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem Disjoint.cycleType_noncommProd {ι : Type*} {k : ι → Perm α} {s : Finset ι}
    (hs : Set.Pairwise s fun i j ↦ Disjoint (k i) (k j))
    (hs' : Set.Pairwise s fun i j ↦ Commute (k i) (k j) :=
      hs.imp (fun _ _ ↦ Perm.Disjoint.commute)) :
    (s.noncommProd k hs').cycleType = s.sum fun i ↦ (k i).cycleType

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j))
    (hs' : optParam ((↑s).Pairwise fun i j => Commute (k i) (k j)) ⋯),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (k j)
hs' : optParam ((↑(insert i s)).Pairwise fun i j => Commute (k i) (k j)) ⋯
⊢ ↑s ⊆ ↑(insert i s)

Tactic:
simp only [Finset.coe_insert, Set.subset_insert]

Result:
no goals

Proof state:
case empty
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
hs : (↑∅).Pairwise fun i j => (k i).Disjoint (k j)
hs' : optParam ((↑∅).Pairwise fun i j => Commute (k i) (k j)) ⋯
⊢ (∅.noncommProd k hs').cycleType = ∑ i ∈ ∅, (k i).cycleType

Tactic:
simp

Result:
no goals

Proof state:
case insert
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j))
    (hs' : optParam ((↑s).Pairwise fun i j => Commute (k i) (k j)) ⋯),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (k j)
hs'✝ : optParam ((↑(insert i s)).Pairwise fun i j => Commute (k i) (k j)) ⋯
hs' : (↑s).Pairwise fun i j => (k i).Disjoint (k j)
⊢ (k i * s.noncommProd k ⋯).cycleType = (k i).cycleType + ∑ x ∈ s, (k x).cycleType

Tactic:
rw [Equiv.Perm.Disjoint.cycleType_mul, hrec hs']

Result:
case insert
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ι : Type u_2
k : ι → Perm α
i : ι
s : Finset ι
hi : i ∉ s
hrec :
  ∀ (hs : (↑s).Pairwise fun i j => (k i).Disjoint (k j))
    (hs' : optParam ((↑s).Pairwise fun i j => Commute (k i) (k j)) ⋯),
    (s.noncommProd k hs').cycleType = ∑ i ∈ s, (k i).cycleType
hs : (↑(insert i s)).Pairwise fun i j => (k i).Disjoint (k j)
hs'✝ : optParam ((↑(insert i s)).Pairwise fun i j => Commute (k i) (k j)) ⋯
hs' : (↑s).Pairwise fun i j => (k i).Disjoint (k j)
⊢ (k i).Disjoint (s.noncommProd k ⋯)
-- Mathlib/Data/List/Basic.lean
theorem getLast_append_of_right_ne_nil (l₁ l₂ : List α) (h : l₂ ≠ []) :
    getLast (l₁ ++ l₂) (append_ne_nil_of_right_ne_nil l₁ h) = getLast l₂ h

Proof state:
case cons
α : Type u
l₂ : List α
h : l₂ ≠ []
head✝ : α
tail✝ : List α
ih : (tail✝ ++ l₂).getLast ⋯ = l₂.getLast h
⊢ (tail✝ ++ l₂).getLast ?cons = l₂.getLast h

case cons
α : Type u
l₂ : List α
h : l₂ ≠ []
head✝ : α
tail✝ : List α
ih : (tail✝ ++ l₂).getLast ⋯ = l₂.getLast h
⊢ tail✝ ++ l₂ ≠ []

Tactic:
exact ih

Result:
no goals

Proof state:
case cons
α : Type u
l₂ : List α
h : l₂ ≠ []
head✝ : α
tail✝ : List α
ih : (tail✝ ++ l₂).getLast ⋯ = l₂.getLast h
⊢ (head✝ :: (tail✝ ++ l₂)).getLast ⋯ = l₂.getLast h

Tactic:
rw [List.getLast_cons]

Result:
case cons
α : Type u
l₂ : List α
h : l₂ ≠ []
head✝ : α
tail✝ : List α
ih : (tail✝ ++ l₂).getLast ⋯ = l₂.getLast h
⊢ (tail✝ ++ l₂).getLast ?cons = l₂.getLast h

case cons
α : Type u
l₂ : List α
h : l₂ ≠ []
head✝ : α
tail✝ : List α
ih : (tail✝ ++ l₂).getLast ⋯ = l₂.getLast h
⊢ tail✝ ++ l₂ ≠ []

Proof state:
α : Type u
l₁ l₂ : List α
h : l₂ ≠ []
⊢ (l₁ ++ l₂).getLast ⋯ = l₂.getLast h

Tactic:
induction l₁ with
| nil => simp
| cons _ _ ih => simp only [cons_append]; rw [List.getLast_cons]; exact ih

Result:
no goals

Proof state:
case nil
α : Type u
l₂ : List α
h : l₂ ≠ []
⊢ ([] ++ l₂).getLast ⋯ = l₂.getLast h

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u
l₂ : List α
h : l₂ ≠ []
head✝ : α
tail✝ : List α
ih : (tail✝ ++ l₂).getLast ⋯ = l₂.getLast h
⊢ (head✝ :: tail✝ ++ l₂).getLast ⋯ = l₂.getLast h

Tactic:
simp only [cons_append]

Result:
case cons
α : Type u
l₂ : List α
h : l₂ ≠ []
head✝ : α
tail✝ : List α
ih : (tail✝ ++ l₂).getLast ⋯ = l₂.getLast h
⊢ (head✝ :: (tail✝ ++ l₂)).getLast ⋯ = l₂.getLast h
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
lemma f_le_g_nat (k : ℕ) {a t : ℝ} (ha : 0 ≤ a) (ht : 0 < t) (n : ℕ) :
    ‖f_nat k a t n‖ ≤ g_nat k a t n

Proof state:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ 0 ≤ (↑n + a) ^ k

Tactic:
positivity

Result:
no goals

Proof state:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ 0 ≤ (↑n + a) ^ k * rexp (-π * (↑n + a) ^ 2 * t)

Tactic:
positivity

Result:
no goals

Proof state:
case h.e'_4
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
u : ↑n ≤ ↑n ^ 2
⊢ (↑n + a) ^ 2 - (↑n + a ^ 2) = ↑n ^ 2 - ↑n + 2 * ↑n * a

Tactic:
ring

Result:
no goals

Proof state:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ ↑n ≤ ↑n ^ 2

Tactic:
simpa only [← Nat.cast_pow, Nat.cast_le] using Nat.le_self_pow two_ne_zero _

Result:
no goals

Proof state:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
u : ↑n ≤ ↑n ^ 2
⊢ 0 ≤ (↑n + a) ^ 2 - (↑n + a ^ 2)

Tactic:
convert add_nonneg (sub_nonneg.mpr u) (by positivity : 0 ≤ 2 * n * a) using 1

Result:
case h.e'_4
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
u : ↑n ≤ ↑n ^ 2
⊢ (↑n + a) ^ 2 - (↑n + a ^ 2) = ↑n ^ 2 - ↑n + 2 * ↑n * a

Proof state:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
u : ↑n ≤ ↑n ^ 2
⊢ 0 ≤ 2 * ↑n * a

Tactic:
positivity

Result:
no goals

Proof state:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ (↑n + a) ^ k * rexp (-π * (↑n + a) ^ 2 * t) ≤ g_nat k a t n

Tactic:
refine mul_le_mul_of_nonneg_left ?_ (by positivity)

Result:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ rexp (-π * (↑n + a) ^ 2 * t) ≤ rexp (-π * (↑n + a ^ 2) * t)

Proof state:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ 0 ≤ (↑n + a) ^ 2 - (↑n + a ^ 2)

Tactic:
have u : (n : ℝ) ≤ (n : ℝ) ^ 2 := by
  simpa only [← Nat.cast_pow, Nat.cast_le] using Nat.le_self_pow two_ne_zero _

Result:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
u : ↑n ≤ ↑n ^ 2
⊢ 0 ≤ (↑n + a) ^ 2 - (↑n + a ^ 2)

Proof state:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ ‖f_nat k a t n‖ ≤ g_nat k a t n

Tactic:
rw [f_nat, norm_of_nonneg (by positivity)]

Result:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ (↑n + a) ^ k * rexp (-π * (↑n + a) ^ 2 * t) ≤ g_nat k a t n

Proof state:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ rexp (-π * (↑n + a) ^ 2 * t) ≤ rexp (-π * (↑n + a ^ 2) * t)

Tactic:
rw [Real.exp_le_exp, mul_le_mul_right ht,
  mul_le_mul_left_of_neg (neg_lt_zero.mpr pi_pos), ← sub_nonneg]

Result:
k : ℕ
a t : ℝ
ha : 0 ≤ a
ht : 0 < t
n : ℕ
⊢ 0 ≤ (↑n + a) ^ 2 - (↑n + a ^ 2)
-- Mathlib/Logic/Function/Basic.lean
theorem not_surjective_Type {α : Type u} (f : α → Type max u v) : ¬Surjective f

Proof state:
case intro
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
⊢ False

Tactic:
let g : Set T → T := fun s ↦ ⟨U, cast hU.symm s⟩

Result:
case intro
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => ⟨U, cast ⋯ s⟩
⊢ False

Proof state:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => ⟨U, cast ⋯ s⟩
s t : Set T
h : g s = g t
this : s = t
⊢ s = t

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => ⟨U, cast ⋯ s⟩
⊢ Injective g

Tactic:
intro s t h

Result:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => ⟨U, cast ⋯ s⟩
s t : Set T
h : g s = g t
⊢ s = t

Proof state:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => ⟨U, cast ⋯ s⟩
s t : Set T
h : g s = g t
this : cast hU (g s).snd = cast hU (g t).snd
⊢ s = t

Tactic:
simp only [g, cast_cast, cast_eq] at this

Result:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => ⟨U, cast ⋯ s⟩
s t : Set T
h : g s = g t
this : s = t
⊢ s = t

Proof state:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => ⟨U, cast ⋯ s⟩
s t : Set T
h : g s = g t
⊢ cast hU (g s).snd = cast hU (g t).snd

Tactic:
congr

Result:
no goals

Proof state:
α : Type u
f : α → Type (max u v)
⊢ ¬Surjective f

Tactic:
intro hf

Result:
α : Type u
f : α → Type (max u v)
hf : Surjective f
⊢ False

Proof state:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => ⟨U, cast ⋯ s⟩
s t : Set T
h : g s = g t
⊢ s = t

Tactic:
suffices cast hU (g s).2 = cast hU (g t).2 by
  simp only [g, cast_cast, cast_eq] at this
  assumption

Result:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => ⟨U, cast ⋯ s⟩
s t : Set T
h : g s = g t
⊢ cast hU (g s).snd = cast hU (g t).snd

Proof state:
case intro
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => ⟨U, cast ⋯ s⟩
hg : Injective g
⊢ False

Tactic:
exact cantor_injective g hg

Result:
no goals

Proof state:
α : Type u
f : α → Type (max u v)
hf : Surjective f
⊢ False

Tactic:
let T : Type max u v := Sigma f

Result:
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
⊢ False
-- Mathlib/LinearAlgebra/LinearDisjoint.lean
theorem not_linearIndependent_pair_of_commute_of_flat (hf : Module.Flat R M ∨ Module.Flat R N)
    (a b : ↥(M ⊓ N)) (hc : Commute a.1 b.1) : ¬LinearIndependent R ![a, b]

Proof state:
case inl
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Nontrivial R
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h✝ : Module.Flat R ↥M
⊢ ¬LinearIndependent R ![a, b]

Tactic:
exact H.not_linearIndependent_pair_of_commute_of_flat_left a b hc

Result:
no goals

Proof state:
case inr
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Nontrivial R
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h✝ : Module.Flat R ↥N
⊢ ¬LinearIndependent R ![a, b]

Tactic:
exact H.not_linearIndependent_pair_of_commute_of_flat_right a b hc

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Nontrivial R
hf : Module.Flat R ↥M ∨ Module.Flat R ↥N
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
⊢ ¬LinearIndependent R ![a, b]

Tactic:
rcases hf with _ | _

Result:
case inl
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Nontrivial R
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h✝ : Module.Flat R ↥M
⊢ ¬LinearIndependent R ![a, b]

case inr
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
inst✝¹ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
inst✝ : Nontrivial R
a b : ↥(M ⊓ N)
hc : Commute ↑a ↑b
h✝ : Module.Flat R ↥N
⊢ ¬LinearIndependent R ![a, b]
-- Mathlib/Computability/Primrec.lean
theorem encode : ∀ {n}, @Primrec' n encode
  | 0 => (const 0).of_eq fun v => by rw [v.eq_nil]; rfl
  | _ + 1 =>
    (succ.comp₁ _ (natPair.comp₂ _ head (tail Primrec'.encode))).of_eq fun ⟨_ :: _, _⟩ => rfl

Proof state:
v : List.Vector ℕ 0
⊢ 0 = encode v

Tactic:
rw [v.eq_nil]

Result:
v : List.Vector ℕ 0
⊢ 0 = encode nil

Proof state:
v : List.Vector ℕ 0
⊢ 0 = encode nil

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem mem_direction_iff_eq_vsub_left {s : AffineSubspace k P} {p : P} (hp : p ∈ s) (v : V) :
    v ∈ s.direction ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ v ∈ s.direction ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂

Tactic:
rw [← SetLike.mem_coe, coe_direction_eq_vsub_set_left hp]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ v ∈ (fun x => p -ᵥ x) '' ↑s ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
p : P
hp : p ∈ s
v : V
⊢ v ∈ (fun x => p -ᵥ x) '' ↑s ↔ ∃ p₂ ∈ s, v = p -ᵥ p₂

Tactic:
exact ⟨fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩, fun ⟨p₂, hp₂, hv⟩ => ⟨p₂, hp₂, hv.symm⟩⟩

Result:
no goals
-- Mathlib/LinearAlgebra/SModEq.lean
lemma pow {I : Ideal A} {x y : A} (n : ℕ) (hxy : x ≡ y [SMOD I]) :
    x ^ n ≡ y ^ n [SMOD I]

Proof state:
A : Type u_2
inst✝ : CommRing A
I : Ideal A
x y : A
n : ℕ
hxy : x ≡ y [SMOD I]
⊢ x ^ n ≡ y ^ n [SMOD I]

Tactic:
simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_pow] at hxy ⊢

Result:
A : Type u_2
inst✝ : CommRing A
I : Ideal A
x y : A
n : ℕ
hxy : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
⊢ (Ideal.Quotient.mk I) x ^ n = (Ideal.Quotient.mk I) y ^ n

Proof state:
A : Type u_2
inst✝ : CommRing A
I : Ideal A
x y : A
n : ℕ
hxy : (Ideal.Quotient.mk I) x = (Ideal.Quotient.mk I) y
⊢ (Ideal.Quotient.mk I) x ^ n = (Ideal.Quotient.mk I) y ^ n

Tactic:
rw [hxy]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem mkConst_decl_eq (aig : AIG α) (val : Bool) (idx : Nat) {h : idx < aig.decls.size} :
    have := mkConst_le_size aig val
    (aig.mkConst val).aig.decls[idx]'(by omega) = aig.decls[idx]

Proof state:
case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
⊢ let_fun this := ⋯;
  (aig.mkConst val).aig.decls[idx] = aig.decls[idx]

Tactic:
simp only [mkConst, Array.getElem_push]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
⊢ (if h : idx < aig.decls.size then aig.decls[idx] else Decl.const val) = aig.decls[idx]

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
⊢ (if h : idx < aig.decls.size then aig.decls[idx] else Decl.const val) = aig.decls[idx]

Tactic:
split

Result:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h h✝ : idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

case isFalse
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
h✝ : ¬idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h : idx < aig.decls.size
this : aig.decls.size ≤ (aig.mkConst val).aig.decls.size
⊢ idx < (aig.mkConst val).aig.decls.size

Tactic:
omega

Result:
no goals

Proof state:
case isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
val : Bool
idx : Nat
h h✝ : idx < aig.decls.size
⊢ aig.decls[idx] = aig.decls[idx]

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/NormedSpace/ENormedSpace.lean
theorem map_neg (x : V) : e (-x) = e x :=
  calc
    e (-x) = ‖(-1 : 𝕜)‖₊ * e x

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENormedSpace 𝕜 V
x : V
⊢ ↑‖-1‖₊ * ↑e x = ↑e x

Tactic:
simp

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENormedSpace 𝕜 V
x : V
⊢ ↑e (-x) = ↑‖-1‖₊ * ↑e x

Tactic:
rw [← map_smul, neg_one_smul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/AC.lean
theorem insert_nonEmpty : insert x xs ≠ []

Proof state:
case cons
x✝ x : Nat
xs : List Nat
tail_ih✝ : insert x✝ xs ≠ []
⊢ insert x✝ (x :: xs) ≠ []

Tactic:
simp [insert]

Result:
case cons
x✝ x : Nat
xs : List Nat
tail_ih✝ : insert x✝ xs ≠ []
⊢ ¬(if x✝ < x then x✝ :: x :: xs else x :: insert x✝ xs) = []

Proof state:
case cons
x✝ x : Nat
xs : List Nat
tail_ih✝ : insert x✝ xs ≠ []
⊢ ¬(if x✝ < x then x✝ :: x :: xs else x :: insert x✝ xs) = []

Tactic:
split <;> simp

Result:
no goals

Proof state:
case nil
x : Nat
⊢ insert x [] ≠ []

Tactic:
simp [insert]

Result:
no goals

Proof state:
x : Nat
xs : List Nat
⊢ insert x xs ≠ []

Tactic:
induction xs with
| nil => simp [insert]
| cons x xs _  => simp [insert]; split <;> simp

Result:
no goals
-- Mathlib/Order/Booleanisation.lean
@[simp] lemma lift_lt_lift : lift a < lift b ↔ a < b := ⟨by rintro ⟨_⟩; assumption, LT.lift⟩

Proof state:
case lift
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : a < b
⊢ a < b

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ lift a < lift b → a < b

Tactic:
rintro ⟨_⟩

Result:
case lift
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : a < b
⊢ a < b
-- Mathlib/LinearAlgebra/TensorProduct/Submodule.lean
theorem mulMap_map_comp_eq {T : Type w} [Semiring T] [Algebra R T]
    {F : Type*} [FunLike F S T] [AlgHomClass F R S T] (f : F) :
    mulMap (M.map f) (N.map f) ∘ₗ
      TensorProduct.map ((f : S →ₗ[R] T).submoduleMap M) ((f : S →ₗ[R] T).submoduleMap N)
        = f ∘ₗ mulMap M N

Proof state:
case a.h.h
R : Type u
S : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
M N : Submodule R S
T : Type w
inst✝³ : Semiring T
inst✝² : Algebra R T
F : Type u_1
inst✝¹ : FunLike F S T
inst✝ : AlgHomClass F R S T
f : F
x✝¹ : ↥M
x✝ : ↥N
⊢ ((TensorProduct.AlgebraTensorModule.curry
          ((map f M).mulMap (map f N) ∘ₗ TensorProduct.map ((↑f).submoduleMap M) ((↑f).submoduleMap N)))
        x✝¹)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (↑f ∘ₗ M.mulMap N)) x✝¹) x✝

Tactic:
simp only [TensorProduct.AlgebraTensorModule.curry_apply, LinearMap.restrictScalars_comp,
  TensorProduct.curry_apply, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
  Function.comp_apply, TensorProduct.map_tmul, mulMap_tmul, LinearMap.coe_coe, map_mul]

Result:
case a.h.h
R : Type u
S : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
M N : Submodule R S
T : Type w
inst✝³ : Semiring T
inst✝² : Algebra R T
F : Type u_1
inst✝¹ : FunLike F S T
inst✝ : AlgHomClass F R S T
f : F
x✝¹ : ↥M
x✝ : ↥N
⊢ ↑(((↑f).submoduleMap M) x✝¹) * ↑(((↑f).submoduleMap N) x✝) = f ↑x✝¹ * f ↑x✝

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
M N : Submodule R S
T : Type w
inst✝³ : Semiring T
inst✝² : Algebra R T
F : Type u_1
inst✝¹ : FunLike F S T
inst✝ : AlgHomClass F R S T
f : F
⊢ (map f M).mulMap (map f N) ∘ₗ TensorProduct.map ((↑f).submoduleMap M) ((↑f).submoduleMap N) = ↑f ∘ₗ M.mulMap N

Tactic:
ext

Result:
case a.h.h
R : Type u
S : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
M N : Submodule R S
T : Type w
inst✝³ : Semiring T
inst✝² : Algebra R T
F : Type u_1
inst✝¹ : FunLike F S T
inst✝ : AlgHomClass F R S T
f : F
x✝¹ : ↥M
x✝ : ↥N
⊢ ((TensorProduct.AlgebraTensorModule.curry
          ((map f M).mulMap (map f N) ∘ₗ TensorProduct.map ((↑f).submoduleMap M) ((↑f).submoduleMap N)))
        x✝¹)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (↑f ∘ₗ M.mulMap N)) x✝¹) x✝

Proof state:
case a.h.h
R : Type u
S : Type v
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
M N : Submodule R S
T : Type w
inst✝³ : Semiring T
inst✝² : Algebra R T
F : Type u_1
inst✝¹ : FunLike F S T
inst✝ : AlgHomClass F R S T
f : F
x✝¹ : ↥M
x✝ : ↥N
⊢ ↑(((↑f).submoduleMap M) x✝¹) * ↑(((↑f).submoduleMap N) x✝) = f ↑x✝¹ * f ↑x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem flatten_eq_flatMap {L : Array (Array α)} : flatten L = L.flatMap id

Proof state:
case of
α : Type u_1
xss✝ : List (List α)
⊢ (List.flatMap id xss✝).toArray = flatMap id (List.map List.toArray xss✝).toArray

Tactic:
simp [List.flatMap_map]

Result:
no goals

Proof state:
α : Type u_1
L : Array (Array α)
⊢ L.flatten = flatMap id L

Tactic:
induction L using array₂_induction

Result:
case of
α : Type u_1
xss✝ : List (List α)
⊢ (List.map List.toArray xss✝).toArray.flatten = flatMap id (List.map List.toArray xss✝).toArray

Proof state:
case of
α : Type u_1
xss✝ : List (List α)
⊢ (List.map List.toArray xss✝).toArray.flatten = flatMap id (List.map List.toArray xss✝).toArray

Tactic:
rw [flatten_toArray_map, List.flatten_eq_flatMap]

Result:
case of
α : Type u_1
xss✝ : List (List α)
⊢ (List.flatMap id xss✝).toArray = flatMap id (List.map List.toArray xss✝).toArray
-- Mathlib/Data/Nat/Choose/Basic.lean
@[simp]
lemma choose_one_right (n : ℕ) : choose n 1 = n

Proof state:
n : ℕ
⊢ n.choose 1 = n

Tactic:
induction n <;> simp [*, choose, Nat.add_comm]

Result:
no goals
-- Mathlib/Tactic/NormNum/LegendreSymbol.lean
theorem jacobiSymNat.zero_left (b : ℕ) (hb : Nat.beq (b / 2) 0 = false) : jacobiSymNat 0 b = 0

Proof state:
b : ℕ
hb : (b / 2).beq 0 = false
⊢ 1 < 2 * 1

Tactic:
decide

Result:
no goals

Proof state:
b : ℕ
hb : (b / 2).beq 0 = false
⊢ 1 < b

Tactic:
calc
  1 < 2 * 1       := by decide
  _ ≤ 2 * (b / 2) :=
    Nat.mul_le_mul_left _ (Nat.succ_le.mpr (Nat.pos_of_ne_zero (Nat.ne_of_beq_eq_false hb)))
  _ ≤ b           := Nat.mul_div_le b 2

Result:
no goals

Proof state:
b : ℕ
hb : (b / 2).beq 0 = false
⊢ jacobiSymNat 0 b = 0

Tactic:
rw [jacobiSymNat, Nat.cast_zero, jacobiSym.zero_left ?_]

Result:
b : ℕ
hb : (b / 2).beq 0 = false
⊢ 1 < b