harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem Cache.IsExtensionBy_trans_left (cache1 : Cache aig cnf1) (cache2 : Cache aig cnf2)
    (cache3 : Cache aig cnf3) (h12 : IsExtensionBy cache1 cache2 new1 hnew1)
    (h23 : IsExtensionBy cache2 cache3 new2 hnew2) : IsExtensionBy cache1 cache3 new1 hnew1

Proof state:
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
⊢ cache1.IsExtensionBy cache3 new1 hnew1

Tactic:
apply IsExtensionBy.mk

Result:
case extension
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
⊢ ∀ (idx : Nat) (hidx : idx < aig.decls.size), cache1.marks[idx] = true → cache3.marks[idx] = true

case trueAt
aig : AIG Nat
cnf1 cnf2 cnf3 : CNF aig.CNFVar
new1 : Nat
hnew1 : new1 < aig.decls.size
new2 : Nat
hnew2 : new2 < aig.decls.size
cache1 : Cache aig cnf1
cache2 : Cache aig cnf2
cache3 : Cache aig cnf3
h12 : cache1.IsExtensionBy cache2 new1 hnew1
h23 : cache2.IsExtensionBy cache3 new2 hnew2
⊢ cache3.marks[new1] = true
-- Mathlib/RingTheory/Jacobson/Ideal.lean
theorem mem_jacobson_iff {x : R} : x ∈ jacobson I ↔ ∀ y, ∃ z, z * y * x + z - 1 ∈ I :=
  ⟨fun hx y =>
    by_cases
      (fun hxy : I ⊔ span {y * x + 1} = ⊤ =>
        let ⟨p, hpi, q, hq, hpq⟩ := Submodule.mem_sup.1 ((eq_top_iff_one _).1 hxy)
        let ⟨r, hr⟩ := mem_span_singleton'.1 hq
        ⟨r, by
          rw [mul_assoc, ← mul_add_one, hr, ← hpq, ← neg_sub, add_sub_cancel_right]
          exact I.neg_mem hpi⟩)
      fun hxy : I ⊔ span {y * x + 1} ≠ ⊤ => let ⟨M, hm1, hm2⟩ := exists_le_maximal _ hxy
      suffices x ∉ M from (this <| mem_sInf.1 hx ⟨le_trans le_sup_left hm2, hm1⟩).elim
      fun hxm => hm1.1.1 <| (eq_top_iff_one _).2 <| add_sub_cancel_left (y * x) 1 ▸
        M.sub_mem (le_sup_right.trans hm2 <| subset_span rfl) (M.mul_mem_left _ hxm),
    fun hx => mem_sInf.2 fun M ⟨him, hm⟩ => by_contradiction fun hxm =>
      let ⟨y, i, hi, df⟩ := hm.exists_inv hxm
      let ⟨z, hz⟩ := hx (-y)
      hm.1.1 <| (eq_top_iff_one _).2 <| sub_sub_cancel (z * -y * x + z) 1 ▸
        M.sub_mem (by
          rw [mul_assoc, ← mul_add_one, neg_mul, ← sub_eq_iff_eq_add.mpr df.symm, neg_sub,
            sub_add_cancel]
          exact M.mul_mem_left _ hi) <| him hz⟩

Proof state:
R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : x ∈ I.jacobson
y : R
hxy : I ⊔ span {y * x + 1} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {y * x + 1}
hpq : p + q = 1
r : R
hr : r * (y * x + 1) = q
⊢ -p ∈ I

Tactic:
exact I.neg_mem hpi

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
M : Ideal R
x✝ : M ∈ {J | I ≤ J ∧ J.IsMaximal}
him : I ≤ M
hm : M.IsMaximal
hxm : x ∉ M
y i : R
hi : i ∈ M
df : y * x + i = 1
z : R
hz : z * -y * x + z - 1 ∈ I
⊢ z * -y * x + z ∈ M

Tactic:
rw [mul_assoc, ← mul_add_one, neg_mul, ← sub_eq_iff_eq_add.mpr df.symm, neg_sub,
  sub_add_cancel]

Result:
R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
M : Ideal R
x✝ : M ∈ {J | I ≤ J ∧ J.IsMaximal}
him : I ≤ M
hm : M.IsMaximal
hxm : x ∉ M
y i : R
hi : i ∈ M
df : y * x + i = 1
z : R
hz : z * -y * x + z - 1 ∈ I
⊢ z * i ∈ M

Proof state:
R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
M : Ideal R
x✝ : M ∈ {J | I ≤ J ∧ J.IsMaximal}
him : I ≤ M
hm : M.IsMaximal
hxm : x ∉ M
y i : R
hi : i ∈ M
df : y * x + i = 1
z : R
hz : z * -y * x + z - 1 ∈ I
⊢ z * i ∈ M

Tactic:
exact M.mul_mem_left _ hi

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : x ∈ I.jacobson
y : R
hxy : I ⊔ span {y * x + 1} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {y * x + 1}
hpq : p + q = 1
r : R
hr : r * (y * x + 1) = q
⊢ r * y * x + r - 1 ∈ I

Tactic:
rw [mul_assoc, ← mul_add_one, hr, ← hpq, ← neg_sub, add_sub_cancel_right]

Result:
R : Type u
inst✝ : Ring R
I : Ideal R
x : R
hx : x ∈ I.jacobson
y : R
hxy : I ⊔ span {y * x + 1} = ⊤
p : R
hpi : p ∈ I
q : R
hq : q ∈ span {y * x + 1}
hpq : p + q = 1
r : R
hr : r * (y * x + 1) = q
⊢ -p ∈ I
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem moebius_sq {n : ℕ} :
    μ n ^ 2 = if Squarefree n then 1 else 0

Proof state:
case neg
n : ℕ
h : ¬Squarefree n
⊢ μ n ^ 2 = 0

Tactic:
simp only [pow_eq_zero_iff, moebius_eq_zero_of_not_squarefree h,
zero_pow (show 2 ≠ 0 by norm_num)]

Result:
no goals

Proof state:
case pos
n : ℕ
h : Squarefree n
⊢ μ n ^ 2 = 1

Tactic:
exact moebius_sq_eq_one_of_squarefree h

Result:
no goals

Proof state:
n : ℕ
⊢ μ n ^ 2 = if Squarefree n then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
n : ℕ
h : Squarefree n
⊢ μ n ^ 2 = 1

case neg
n : ℕ
h : ¬Squarefree n
⊢ μ n ^ 2 = 0

Proof state:
n : ℕ
h : ¬Squarefree n
⊢ 2 ≠ 0

Tactic:
norm_num

Result:
no goals
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t` for `t ≠ 0`, then `ω ↦ |X ω| ^ n` is
integrable for all `n : ℕ`. That is, all moments of `X` are finite. -/
lemma integrable_pow_abs_of_integrable_exp_mul (ht : t ≠ 0)
    (ht_int_pos : Integrable (fun ω ↦ exp (t * X ω)) μ)
    (ht_int_neg : Integrable (fun ω ↦ exp (- t * X ω)) μ) (n : ℕ) :
    Integrable (fun ω ↦ |X ω| ^ n) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
n : ℕ
⊢ Integrable (fun ω => |X ω| ^ n) μ

Tactic:
convert integrable_rpow_abs_of_integrable_exp_mul ht ht_int_pos ht_int_neg
  (by positivity : 0 ≤ (n : ℝ)) with ω

Result:
case h.e'_6.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
n : ℕ
ω : Ω
⊢ |X ω| ^ n = |X ω| ^ ↑n

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
n : ℕ
⊢ 0 ≤ ↑n

Tactic:
positivity

Result:
no goals

Proof state:
case h.e'_6.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ≠ 0
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
n : ℕ
ω : Ω
⊢ |X ω| ^ n = |X ω| ^ ↑n

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Covering/OneDim.lean
theorem tendsto_Icc_vitaliFamily_left (x : ℝ) :
    Tendsto (fun y => Icc y x) (𝓝[<] x) ((vitaliFamily (volume : Measure ℝ) 1).filterAt x)

Proof state:
case h
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ Icc y x ⊆ Metric.closedBall x ε

Tactic:
rw [closedBall_eq_Icc]

Result:
case h
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ Icc y x ⊆ Icc (x - ε) (x + ε)

Proof state:
case refine_2
x : ℝ
⊢ ∀ ε > 0, ∀ᶠ (i : ℝ) in 𝓝[<] x, Icc i x ⊆ Metric.closedBall x ε

Tactic:
intro ε εpos

Result:
case refine_2
x ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (i : ℝ) in 𝓝[<] x, Icc i x ⊆ Metric.closedBall x ε

Proof state:
case refine_1
x : ℝ
⊢ ∀ᶠ (i : ℝ) in 𝓝[<] x, Icc i x ∈ (vitaliFamily volume 1).setsAt x

Tactic:
filter_upwards [self_mem_nhdsWithin] with y hy using Icc_mem_vitaliFamily_at_left hy

Result:
no goals

Proof state:
case refine_2
x ε : ℝ
εpos : ε > 0
⊢ ∀ᶠ (i : ℝ) in 𝓝[<] x, Icc i x ⊆ Metric.closedBall x ε

Tactic:
filter_upwards [Icc_mem_nhdsLT <| show x - ε < x by linarith] with y hy

Result:
case h
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ Icc y x ⊆ Metric.closedBall x ε

Proof state:
x : ℝ
⊢ Tendsto (fun y => Icc y x) (𝓝[<] x) ((vitaliFamily volume 1).filterAt x)

Tactic:
refine (VitaliFamily.tendsto_filterAt_iff _).2 ⟨?_, ?_⟩

Result:
case refine_1
x : ℝ
⊢ ∀ᶠ (i : ℝ) in 𝓝[<] x, Icc i x ∈ (vitaliFamily volume 1).setsAt x

case refine_2
x : ℝ
⊢ ∀ ε > 0, ∀ᶠ (i : ℝ) in 𝓝[<] x, Icc i x ⊆ Metric.closedBall x ε

Proof state:
x ε : ℝ
εpos : ε > 0
⊢ x - ε < x

Tactic:
linarith

Result:
no goals

Proof state:
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ x ≤ x + ε

Tactic:
linarith

Result:
no goals

Proof state:
case h
x ε : ℝ
εpos : ε > 0
y : ℝ
hy : y ∈ Icc (x - ε) x
⊢ Icc y x ⊆ Icc (x - ε) (x + ε)

Tactic:
exact Icc_subset_Icc hy.1 (by linarith)

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicIntegers.lean
@[simp] lemma coe_eq_zero : (x : ℚ_[p]) = 0 ↔ x = 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
⊢ ↑x = 0 ↔ x = 0

Tactic:
rw [← coe_zero, Subtype.coe_inj]

Result:
no goals
-- Mathlib/Algebra/Algebra/Defs.lean
theorem mul_smul_comm (s : R) (x y : A) : x * s • y = s • (x * y)

Proof state:
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : R
x y : A
⊢ x * s • y = s • (x * y)

Tactic:
rw [smul_def, smul_def, left_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional.lean
theorem ker_pow_eq_ker_pow_finrank_of_le [FiniteDimensional K V] {f : End K V} {m : ℕ}
    (hm : finrank K V ≤ m) : LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
hm : finrank K V ≤ m
k : ℕ
h_k_le : k ≤ finrank K V
hk : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
⊢ LinearMap.ker (f ^ m) = LinearMap.ker (f ^ (k + (m - k)))

Tactic:
rw [add_tsub_cancel_of_le (h_k_le.trans hm)]

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
hm : finrank K V ≤ m
⊢ LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)

Tactic:
obtain ⟨k, h_k_le, hk⟩ :
  ∃ k, k ≤ finrank K V ∧ LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ) :=
  exists_ker_pow_eq_ker_pow_succ f

Result:
case intro.intro
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
hm : finrank K V ≤ m
k : ℕ
h_k_le : k ≤ finrank K V
hk : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
⊢ LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)

Proof state:
case intro.intro
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
hm : finrank K V ≤ m
k : ℕ
h_k_le : k ≤ finrank K V
hk : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
⊢ LinearMap.ker (f ^ m) = LinearMap.ker (f ^ finrank K V)

Tactic:
calc
  LinearMap.ker (f ^ m) = LinearMap.ker (f ^ (k + (m - k))) := by
    rw [add_tsub_cancel_of_le (h_k_le.trans hm)]
  _ = LinearMap.ker (f ^ k) := by rw [ker_pow_constant hk _]
  _ = LinearMap.ker (f ^ (k + (finrank K V - k))) := ker_pow_constant hk (finrank K V - k)
  _ = LinearMap.ker (f ^ finrank K V) := by rw [add_tsub_cancel_of_le h_k_le]

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
hm : finrank K V ≤ m
k : ℕ
h_k_le : k ≤ finrank K V
hk : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
⊢ LinearMap.ker (f ^ (k + (finrank K V - k))) = LinearMap.ker (f ^ finrank K V)

Tactic:
rw [add_tsub_cancel_of_le h_k_le]

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
hm : finrank K V ≤ m
k : ℕ
h_k_le : k ≤ finrank K V
hk : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
⊢ LinearMap.ker (f ^ (k + (m - k))) = LinearMap.ker (f ^ k)

Tactic:
rw [ker_pow_constant hk _]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem All.append (hl : l.All p) (hr : r.All p) : (append l r).All p

Proof state:
α✝ : Type u_1
l r : RBNode α✝
p : α✝ → Prop
hl : All p l
hr : All p r
⊢ All p (l.append r)

Tactic:
unfold append

Result:
α✝ : Type u_1
l r : RBNode α✝
p : α✝ → Prop
hl : All p l
hr : All p r
⊢ All p
    (match l, r with
    | nil, x => x
    | x, nil => x
    | node red a x b, node red c y d =>
      match b.append c with
      | node red b' z c' => node red (node red a x b') z (node red c' y d)
      | bc => node red a x (node red bc y d)
    | node black a x b, node black c y d =>
      match b.append c with
      | node red b' z c' => node red (node black a x b') z (node black c' y d)
      | bc => a.balLeft x (node black bc y d)
    | a@h:(node black l v r), node red b x c => node red (a.append b) x c
    | node red a x b, c@h:(node black l v r) => node red a x (b.append c))

Proof state:
case h_5
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ l✝ : RBNode α✝
v✝ : α✝
r✝ b✝ : RBNode α✝
x✝ : α✝
c✝ : RBNode α✝
hl : All p (node black l✝ v✝ r✝)
hr : All p (node red b✝ x✝ c✝)
⊢ p x✝ ∧ All p ((node black l✝ v✝ r✝).append b✝) ∧ All p c✝

Tactic:
simp_all [hl.append hr.2.1]

Result:
no goals

Proof state:
case h_3
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node red c✝ y✝ d✝)
⊢ All p
    (match b✝.append c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))

Tactic:
have ⟨hx, ha, hb⟩ := hl

Result:
case h_3
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node red a✝ x✝ b✝)
hr : All p (node red c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
⊢ All p
    (match b✝.append c✝ with
    | node red b' z c' => node red (node red a✝ x✝ b') z (node red c' y✝ d✝)
    | bc => node red a✝ x✝ (node red bc y✝ d✝))

Proof state:
case h_4
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node black a✝ x✝ b✝)
hr : All p (node black c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
⊢ All p
    (match b✝.append c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => a✝.balLeft x✝ (node black bc y✝ d✝))

Tactic:
have ⟨hy, hc, hd⟩ := hr

Result:
case h_4
α✝ : Type u_1
p : α✝ → Prop
x✝² x✝¹ a✝ : RBNode α✝
x✝ : α✝
b✝ c✝ : RBNode α✝
y✝ : α✝
d✝ : RBNode α✝
hl : All p (node black a✝ x✝ b✝)
hr : All p (node black c✝ y✝ d✝)
hx : p x✝
ha : All p a✝
hb : All p b✝
hy : p y✝
hc : All p c✝
hd : All p d✝
⊢ All p
    (match b✝.append c✝ with
    | node red b' z c' => node red (node black a✝ x✝ b') z (node black c' y✝ d✝)
    | bc => a✝.balLeft x✝ (node black bc y✝ d✝))
-- Mathlib/Data/PFun.lean
theorem mem_prodMap {f : α →. γ} {g : β →. δ} {x : α × β} {y : γ × δ} :
    y ∈ f.prodMap g x ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ y ∈ f.prodMap g x ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2

Tactic:
trans ∃ hp hq, (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ y ∈ f.prodMap g x ↔ ∃ (hp : (f x.1).Dom) (hq : (g x.2).Dom), (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2

α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ (∃ (hp : (f x.1).Dom) (hq : (g x.2).Dom), (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2) ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ (∃ (hp : (f x.1).Dom) (hq : (g x.2).Dom), (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2) ↔ y.1 ∈ f x.1 ∧ y.2 ∈ g x.2

Tactic:
simp only [exists_and_left, exists_and_right, Membership.mem, Part.Mem]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α →. γ
g : β →. δ
x : α × β
y : γ × δ
⊢ y ∈ f.prodMap g x ↔ ∃ (hp : (f x.1).Dom) (hq : (g x.2).Dom), (f x.1).get hp = y.1 ∧ (g x.2).get hq = y.2

Tactic:
simp only [prodMap, Part.mem_mk_iff, And.exists, Prod.ext_iff]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
theorem lift_injective_of_ker_le_ideal (I : Ideal R) [I.IsTwoSided]
    {f : R →+* S} (H : ∀ a : R, a ∈ I → f a = 0)
    (hI : ker f ≤ I) : Function.Injective (Ideal.Quotient.lift I f H)

Proof state:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
⊢ ∀ (x : R ⧸ I), (Ideal.Quotient.lift I f H) x = 0 → x = 0

Tactic:
intro u hu

Result:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
u : R ⧸ I
hu : (Ideal.Quotient.lift I f H) u = 0
⊢ u = 0

Proof state:
case intro
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
v : R
hu : f v = 0
⊢ (Ideal.Quotient.mk I) v = 0

Tactic:
rw [Ideal.Quotient.eq_zero_iff_mem]

Result:
case intro
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
v : R
hu : f v = 0
⊢ v ∈ I

Proof state:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
⊢ Function.Injective ⇑(Ideal.Quotient.lift I f H)

Tactic:
rw [RingHom.injective_iff_ker_eq_bot, RingHom.ker_eq_bot_iff_eq_zero]

Result:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
⊢ ∀ (x : R ⧸ I), (Ideal.Quotient.lift I f H) x = 0 → x = 0

Proof state:
case intro
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
v : R
hu : (Ideal.Quotient.lift I f H) ((Ideal.Quotient.mk I) v) = 0
⊢ (Ideal.Quotient.mk I) v = 0

Tactic:
rw [Ideal.Quotient.lift_mk] at hu

Result:
case intro
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
v : R
hu : f v = 0
⊢ (Ideal.Quotient.mk I) v = 0

Proof state:
case intro
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
v : R
hu : f v = 0
⊢ v ∈ I

Tactic:
exact hI (RingHom.mem_ker.mpr hu)

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
u : R ⧸ I
hu : (Ideal.Quotient.lift I f H) u = 0
⊢ u = 0

Tactic:
obtain ⟨v, rfl⟩ := Ideal.Quotient.mk_surjective u

Result:
case intro
R : Type u
S : Type v
inst✝² : Ring R
inst✝¹ : Semiring S
I : Ideal R
inst✝ : I.IsTwoSided
f : R →+* S
H : ∀ a ∈ I, f a = 0
hI : ker f ≤ I
v : R
hu : (Ideal.Quotient.lift I f H) ((Ideal.Quotient.mk I) v) = 0
⊢ (Ideal.Quotient.mk I) v = 0
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem pi_bot : (pi Set.univ fun i => (⊥ : Subgroup (f i))) = ⊥ :=
  (eq_bot_iff_forall _).mpr fun p hp => by
    simp only [mem_pi, mem_bot] at *
    ext j
    exact hp j trivial

Proof state:
case h
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
p : (i : η) → f i
hp : ∀ i ∈ univ, p i = 1
j : η
⊢ p j = 1 j

Tactic:
exact hp j trivial

Result:
no goals

Proof state:
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
p : (i : η) → f i
hp : ∀ i ∈ univ, p i = 1
⊢ p = 1

Tactic:
ext j

Result:
case h
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
p : (i : η) → f i
hp : ∀ i ∈ univ, p i = 1
j : η
⊢ p j = 1 j

Proof state:
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
p : (i : η) → f i
hp : p ∈ pi univ fun i => ⊥
⊢ p = 1

Tactic:
simp only [mem_pi, mem_bot] at *

Result:
η : Type u_7
f : η → Type u_8
inst✝ : (i : η) → Group (f i)
p : (i : η) → f i
hp : ∀ i ∈ univ, p i = 1
⊢ p = 1
-- Mathlib/Data/List/Permutation.lean
theorem injective_permutations'Aux (x : α) : Function.Injective (permutations'Aux x)

Proof state:
α : Type u_1
x : α
⊢ Injective (permutations'Aux x)

Tactic:
intro s t h

Result:
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
⊢ s = t

Proof state:
case a
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
⊢ insertIdx s.length x s = insertIdx s.length x t

Tactic:
have hl : s.length = t.length := by simpa using congr_arg length h

Result:
case a
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
⊢ insertIdx s.length x s = insertIdx s.length x t

Proof state:
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
⊢ s.length = t.length

Tactic:
simpa using congr_arg length h

Result:
no goals

Proof state:
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
⊢ s = t

Tactic:
apply insertIdx_injective s.length x

Result:
case a
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
⊢ insertIdx s.length x s = insertIdx s.length x t

Proof state:
case a
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
⊢ insertIdx s.length x s = insertIdx s.length x t

Tactic:
rw [← get_permutations'Aux s x s.length (by simp),
  ← get_permutations'Aux t x s.length (by simp [hl])]

Result:
case a
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
⊢ (permutations'Aux x s).get ⟨s.length, ⋯⟩ = (permutations'Aux x t).get ⟨s.length, ⋯⟩

Proof state:
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
⊢ s.length < (permutations'Aux x t).length

Tactic:
simp [hl]

Result:
no goals

Proof state:
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
⊢ s.length < (permutations'Aux x s).length

Tactic:
simp

Result:
no goals

Proof state:
case a
α : Type u_1
x : α
s t : List α
h : permutations'Aux x s = permutations'Aux x t
hl : s.length = t.length
⊢ (permutations'Aux x s).get ⟨s.length, ⋯⟩ = (permutations'Aux x t).get ⟨s.length, ⋯⟩

Tactic:
simp only [get_eq_getElem, h, hl]

Result:
no goals