harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/Trace.lean
theorem traceAux_eq : traceAux R b = traceAux R c :=
  LinearMap.ext fun f =>
    calc
      Matrix.trace (LinearMap.toMatrix b b f) =
          Matrix.trace (LinearMap.toMatrix b b ((LinearMap.id.comp f).comp LinearMap.id))

Proof state:
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ((toMatrix b b) f).trace = ((toMatrix b b) ((id ∘ₗ f) ∘ₗ id)).trace

Tactic:
rw [LinearMap.id_comp, LinearMap.comp_id]

Result:
no goals

Proof state:
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ((toMatrix c c) f * (toMatrix b c) id * (toMatrix c b) id).trace = ((toMatrix c c) ((f ∘ₗ id) ∘ₗ id)).trace

Tactic:
rw [LinearMap.toMatrix_comp _ b, LinearMap.toMatrix_comp _ c]

Result:
no goals

Proof state:
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ((toMatrix b b) ((id ∘ₗ f) ∘ₗ id)).trace = ((toMatrix c b) id * (toMatrix c c) f * (toMatrix b c) id).trace

Tactic:
rw [LinearMap.toMatrix_comp _ c, LinearMap.toMatrix_comp _ c]

Result:
no goals

Proof state:
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ((toMatrix c b) id * (toMatrix c c) f * (toMatrix b c) id).trace =
    ((toMatrix c c) f * (toMatrix b c) id * (toMatrix c b) id).trace

Tactic:
rw [Matrix.mul_assoc, Matrix.trace_mul_comm]

Result:
no goals

Proof state:
R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ((toMatrix c c) ((f ∘ₗ id) ∘ₗ id)).trace = ((toMatrix c c) f).trace

Tactic:
rw [LinearMap.comp_id, LinearMap.comp_id]

Result:
no goals
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eq_zero_of_degree_lt_of_eval_index_eq_zero (hvs : Set.InjOn v s)
    (degree_f_lt : f.degree < #s) (eval_f : ∀ i ∈ s, f.eval (v i) = 0) : f = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#(image v s))
eval_f : ∀ i ∈ s, eval (v i) f = 0
⊢ ∀ x ∈ image v s, eval x f = 0

Tactic:
intro x hx

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#(image v s))
eval_f : ∀ i ∈ s, eval (v i) f = 0
x : R
hx : x ∈ image v s
⊢ eval x f = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#(image v s))
eval_f : ∀ i ∈ s, eval (v i) f = 0
x : R
hx : x ∈ image v s
⊢ eval x f = 0

Tactic:
rcases mem_image.mp hx with ⟨_, hj, rfl⟩

Result:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#(image v s))
eval_f : ∀ i ∈ s, eval (v i) f = 0
w✝ : ι
hj : w✝ ∈ s
hx : v w✝ ∈ image v s
⊢ eval (v w✝) f = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#(image v s))
eval_f : ∀ i ∈ s, eval (v i) f = 0
⊢ f = 0

Tactic:
refine eq_zero_of_degree_lt_of_eval_finset_eq_zero _ degree_f_lt ?_

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#(image v s))
eval_f : ∀ i ∈ s, eval (v i) f = 0
⊢ ∀ x ∈ image v s, eval x f = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#s)
eval_f : ∀ i ∈ s, eval (v i) f = 0
⊢ f = 0

Tactic:
rw [← card_image_of_injOn hvs] at degree_f_lt

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#(image v s))
eval_f : ∀ i ∈ s, eval (v i) f = 0
⊢ f = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#s)
eval_f : ∀ i ∈ s, eval (v i) f = 0
⊢ f = 0

Tactic:
classical
  rw [← card_image_of_injOn hvs] at degree_f_lt
  refine eq_zero_of_degree_lt_of_eval_finset_eq_zero _ degree_f_lt ?_
  intro x hx
  rcases mem_image.mp hx with ⟨_, hj, rfl⟩
  exact eval_f _ hj

Result:
no goals

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
ι : Type u_2
v : ι → R
s : Finset ι
hvs : Set.InjOn v ↑s
degree_f_lt : f.degree < ↑(#(image v s))
eval_f : ∀ i ∈ s, eval (v i) f = 0
w✝ : ι
hj : w✝ ∈ s
hx : v w✝ ∈ image v s
⊢ eval (v w✝) f = 0

Tactic:
exact eval_f _ hj

Result:
no goals
-- Mathlib/Data/Finset/Powerset.lean
lemma pairwiseDisjoint_pair_insert [DecidableEq α] {a : α} (ha : a ∉ s) :
    (s.powerset : Set (Finset α)).PairwiseDisjoint fun t ↦ ({t, insert a t} : Set (Finset α))

Proof state:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j

Tactic:
simp only [Set.Nonempty, Set.mem_inter_iff, Set.mem_insert_iff, Set.mem_singleton_iff,
  exists_eq_or_imp, exists_eq_left, or_imp, imp_self, true_and]

Result:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ (i = insert a j → i = j) ∧ (insert a i = j → i = j) ∧ (insert a i = insert a j → i = j)

Proof state:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ (i = insert a j → i = j) ∧ (insert a i = j → i = j) ∧ (insert a i = insert a j → i = j)

Tactic:
refine ⟨?_, ?_, insert_erase_invOn.2.injOn (not_mem_mono hi ha) (not_mem_mono hj ha)⟩ <;>
  rintro rfl <;>
  cases Finset.not_mem_mono ‹_› ha (Finset.mem_insert_self _ _)

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ (↑s.powerset).PairwiseDisjoint fun t => {t, insert a t}

Tactic:
simp_rw [Set.pairwiseDisjoint_iff, mem_coe, mem_powerset]

Result:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ ∀ ⦃i : Finset α⦄, i ⊆ s → ∀ ⦃j : Finset α⦄, j ⊆ s → ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j

Proof state:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
⊢ ∀ ⦃i : Finset α⦄, i ⊆ s → ∀ ⦃j : Finset α⦄, j ⊆ s → ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j

Tactic:
rintro i hi j hj

Result:
α : Type u_1
s : Finset α
inst✝ : DecidableEq α
a : α
ha : a ∉ s
i : Finset α
hi : i ⊆ s
j : Finset α
hj : j ⊆ s
⊢ ({i, insert a i} ∩ {j, insert a j}).Nonempty → i = j
-- Mathlib/Analysis/Normed/Module/Convex.lean
theorem isConnected_setOf_sameRay (x : E) : IsConnected { y | SameRay ℝ x y }

Proof state:
case pos
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : x = 0
⊢ IsConnected {y | SameRay ℝ x y}

Tactic:
simpa [hx] using isConnected_univ (α := E)

Result:
no goals

Proof state:
case neg
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ¬x = 0
⊢ IsConnected {y | SameRay ℝ x y}

Tactic:
simp_rw [← exists_nonneg_left_iff_sameRay hx]

Result:
case neg
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ¬x = 0
⊢ IsConnected {y | ∃ r, 0 ≤ r ∧ r • x = y}

Proof state:
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
⊢ IsConnected {y | SameRay ℝ x y}

Tactic:
by_cases hx : x = 0

Result:
case pos
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : x = 0
⊢ IsConnected {y | SameRay ℝ x y}

case neg
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ¬x = 0
⊢ IsConnected {y | SameRay ℝ x y}

Proof state:
case neg
E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
x : E
hx : ¬x = 0
⊢ IsConnected {y | ∃ r, 0 ≤ r ∧ r • x = y}

Tactic:
exact isConnected_Ici.image _ (continuous_id.smul continuous_const).continuousOn

Result:
no goals
-- Mathlib/Order/Filter/Finite.lean
theorem iInf_principal {ι : Sort w} [Finite ι] (f : ι → Set α) : ⨅ i, 𝓟 (f i) = 𝓟 (⋂ i, f i)

Proof state:
case intro
α : Type u
ι : Sort w
inst✝ : Finite ι
f : ι → Set α
val✝ : Fintype (PLift ι)
⊢ ⨅ i, 𝓟 (f i) = 𝓟 (⋂ i, f i)

Tactic:
rw [← iInf_plift_down, ← iInter_plift_down]

Result:
case intro
α : Type u
ι : Sort w
inst✝ : Finite ι
f : ι → Set α
val✝ : Fintype (PLift ι)
⊢ ⨅ i, 𝓟 (f i.down) = 𝓟 (⋂ i, f i.down)

Proof state:
α : Type u
ι : Sort w
inst✝ : Finite ι
f : ι → Set α
⊢ ⨅ i, 𝓟 (f i) = 𝓟 (⋂ i, f i)

Tactic:
cases nonempty_fintype (PLift ι)

Result:
case intro
α : Type u
ι : Sort w
inst✝ : Finite ι
f : ι → Set α
val✝ : Fintype (PLift ι)
⊢ ⨅ i, 𝓟 (f i) = 𝓟 (⋂ i, f i)
-- Mathlib/Data/ENNReal/Real.lean
theorem ofReal_lt_coe_iff {a : ℝ} {b : ℝ≥0} (ha : 0 ≤ a) : ENNReal.ofReal a < b ↔ a < b :=
  (ofReal_lt_iff_lt_toReal ha coe_ne_top).trans <| by rw [coe_toReal]

Proof state:
a : ℝ
b : ℝ≥0
ha : 0 ≤ a
⊢ a < (↑b).toReal ↔ a < ↑b

Tactic:
rw [coe_toReal]

Result:
no goals
-- Mathlib/RingTheory/Artinian/Module.lean
lemma isField_of_isDomain [IsDomain R] : IsField R

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = x ^ n • 1
⊢ ∃ b, x * b = 1

Tactic:
replace hy : x ^ n * (x * y - 1) = 0 := by
  rw [mul_sub, sub_eq_zero]
  convert hy using 1
  simp [Nat.succ_eq_add_one, pow_add, mul_assoc]

Result:
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n * (x * y - 1) = 0
⊢ ∃ b, x * b = 1

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n = 0 ∨ x * y = 1
⊢ ∃ b, x * b = 1

Tactic:
exact ⟨_, hy.resolve_left <| pow_ne_zero _ hx⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = x ^ n • 1
⊢ x ^ n * (x * y - 1) = 0

Tactic:
rw [mul_sub, sub_eq_zero]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = x ^ n • 1
⊢ x ^ n * (x * y) = x ^ n * 1

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = x ^ n • 1
⊢ x ^ n * (x * y) = x ^ n * 1

Tactic:
convert hy using 1

Result:
case h.e'_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = x ^ n • 1
⊢ x ^ n * (x * y) = x ^ n.succ • y

Proof state:
case h.e'_2
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = x ^ n • 1
⊢ x ^ n * (x * y) = x ^ n.succ • y

Tactic:
simp [Nat.succ_eq_add_one, pow_add, mul_assoc]

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
⊢ ∃ b, x * b = 1

Tactic:
obtain ⟨n, y, hy⟩ := IsArtinian.exists_pow_succ_smul_dvd x (1 : R)

Result:
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n.succ • y = x ^ n • 1
⊢ ∃ b, x * b = 1

Proof state:
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n * (x * y - 1) = 0
⊢ ∃ b, x * b = 1

Tactic:
rw [mul_eq_zero, sub_eq_zero] at hy

Result:
case intro.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
n : ℕ
y : R
hy : x ^ n = 0 ∨ x * y = 1
⊢ ∃ b, x * b = 1

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
⊢ IsField R

Tactic:
refine ⟨Nontrivial.exists_pair_ne, mul_comm, fun {x} hx ↦ ?_⟩

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsArtinianRing R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
⊢ ∃ b, x * b = 1
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem image_coe_Ici : (some : α → WithTop α) '' Ici a = Ico (a : WithTop α) ⊤

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' Ici a = Ico ↑a ⊤

Tactic:
rw [← preimage_coe_Ici, image_preimage_eq_inter_range, range_coe, Ici_inter_Iio]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsTrail.reverse {u v : V} (p : G.Walk u v) (h : p.IsTrail) : p.reverse.IsTrail

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
h : p.IsTrail
⊢ p.reverse.IsTrail

Tactic:
simpa [isTrail_def] using h

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem strongInductionOn_eq {p : Finset α → Sort*} (s : Finset α)
    (H : ∀ s, (∀ t ⊂ s, p t) → p s) :
    s.strongInductionOn H = H s fun t _ => t.strongInductionOn H

Proof state:
α : Type u_1
p : Finset α → Sort u_4
s : Finset α
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
⊢ s.strongInductionOn H = H s fun t x => t.strongInductionOn H

Tactic:
dsimp only [strongInductionOn]

Result:
α : Type u_1
p : Finset α → Sort u_4
s : Finset α
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
⊢ strongInduction H s = H s fun t x => strongInduction H t

Proof state:
α : Type u_1
p : Finset α → Sort u_4
s : Finset α
H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s
⊢ strongInduction H s = H s fun t x => strongInduction H t

Tactic:
rw [strongInduction]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Nat.lean
theorem card_fintypeIio : Fintype.card (Set.Iio b) = b

Proof state:
b : ℕ
⊢ Fintype.card ↑(Set.Iio b) = b

Tactic:
rw [Fintype.card_ofFinset, card_Iio]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem LiftRel.lex {a b : α ⊕ β} (h : LiftRel r s a b) : Lex r s a b

Proof state:
case inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
a✝¹ c✝ : α
a✝ : r a✝¹ c✝
⊢ Lex r s (inl a✝¹) (inl c✝)

Tactic:
exact Lex.inl ‹_›

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
b✝ d✝ : β
a✝ : s b✝ d✝
⊢ Lex r s (inr b✝) (inr d✝)

Tactic:
exact Lex.inr ‹_›

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
a b : α ⊕ β
h : LiftRel r s a b
⊢ Lex r s a b

Tactic:
cases h

Result:
case inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
a✝¹ c✝ : α
a✝ : r a✝¹ c✝
⊢ Lex r s (inl a✝¹) (inl c✝)

case inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
b✝ d✝ : β
a✝ : s b✝ d✝
⊢ Lex r s (inr b✝) (inr d✝)
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem disjoint_iSup₂_iff {f : ∀ i, κ i → α} :
    Disjoint a (⨆ (i) (j), f i j) ↔ ∀ i j, Disjoint a (f i j)

Proof state:
α : Type u
ι : Sort w
κ : ι → Sort w'
inst✝ : Frame α
a : α
f : (i : ι) → κ i → α
⊢ Disjoint a (⨆ i, ⨆ j, f i j) ↔ ∀ (i : ι) (j : κ i), Disjoint a (f i j)

Tactic:
simp_rw [disjoint_iSup_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Hermitian.lean
theorem IsHermitian.fromBlocks {A : Matrix m m α} {B : Matrix m n α} {C : Matrix n m α}
    {D : Matrix n n α} (hA : A.IsHermitian) (hBC : Bᴴ = C) (hD : D.IsHermitian) :
    (A.fromBlocks B C D).IsHermitian

Proof state:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
⊢ Cᴴ = B

Tactic:
rw [← hBC, conjTranspose_conjTranspose]

Result:
no goals

Proof state:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
hCB : Cᴴ = B
⊢ (Matrix.fromBlocks A B C D)ᴴ = Matrix.fromBlocks A B C D

Tactic:
rw [fromBlocks_conjTranspose, hBC, hCB, hA, hD]

Result:
no goals

Proof state:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
⊢ (Matrix.fromBlocks A B C D).IsHermitian

Tactic:
have hCB : Cᴴ = B := by rw [← hBC, conjTranspose_conjTranspose]

Result:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
hCB : Cᴴ = B
⊢ (Matrix.fromBlocks A B C D).IsHermitian

Proof state:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
hCB : Cᴴ = B
⊢ (Matrix.fromBlocks A B C D).IsHermitian

Tactic:
unfold Matrix.IsHermitian

Result:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : InvolutiveStar α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
hA : A.IsHermitian
hBC : Bᴴ = C
hD : D.IsHermitian
hCB : Cᴴ = B
⊢ (Matrix.fromBlocks A B C D)ᴴ = Matrix.fromBlocks A B C D
-- Mathlib/RingTheory/Noetherian/Basic.lean
theorem isNoetherian_of_fg_of_noetherian {R M} [Ring R] [AddCommGroup M] [Module R M]
    (N : Submodule R M) [I : IsNoetherianRing R] (hN : N.FG) : IsNoetherian R N

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing R
hN : N.FG
⊢ IsNoetherian R ↥N

Tactic:
rw [← Module.Finite.iff_fg] at hN

Result:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing R
hN : Module.Finite R ↥N
⊢ IsNoetherian R ↥N

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
I : IsNoetherianRing R
hN : Module.Finite R ↥N
⊢ IsNoetherian R ↥N

Tactic:
infer_instance

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LSum.lean
theorem splittingOfFinsuppSurjective_splits (f : M →ₗ[R] α →₀ R) (s : Surjective f) :
    f.comp (splittingOfFinsuppSurjective f s) = LinearMap.id

Proof state:
case h.h.h.e_a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ f ((single x 1).sum fun x r => r • ⋯.choose) = single x 1

Tactic:
rw [sum_single_index, one_smul]

Result:
case h.h.h.e_a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ f ⋯.choose = single x 1

case h.h.h.e_a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ 0 • ⋯.choose = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
⊢ f ∘ₗ f.splittingOfFinsuppSurjective s = id

Tactic:
ext x

Result:
case h.h.h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ (((f ∘ₗ f.splittingOfFinsuppSurjective s) ∘ₗ lsingle x) 1) a✝ = ((id ∘ₗ lsingle x) 1) a✝

Proof state:
case h.h.h.e_a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ 0 • ⋯.choose = 0

Tactic:
rw [zero_smul]

Result:
no goals

Proof state:
case h.h.h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ (((f ∘ₗ f.splittingOfFinsuppSurjective s) ∘ₗ lsingle x) 1) a✝ = ((id ∘ₗ lsingle x) 1) a✝

Tactic:
dsimp [splittingOfFinsuppSurjective]

Result:
case h.h.h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ (f ((single x 1).sum fun x r => r • ⋯.choose)) a✝ = (single x 1) a✝

Proof state:
case h.h.h
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ (f ((single x 1).sum fun x r => r • ⋯.choose)) a✝ = (single x 1) a✝

Tactic:
congr

Result:
case h.h.h.e_a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ f ((single x 1).sum fun x r => r • ⋯.choose) = single x 1

Proof state:
case h.h.h.e_a
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
α : Type u_4
f : M →ₗ[R] α →₀ R
s : Surjective ⇑f
x a✝ : α
⊢ f ⋯.choose = single x 1

Tactic:
exact (s (Finsupp.single x 1)).choose_spec

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Ends/Defs.lean
theorem mem_of_adj : ∀ {C : G.ComponentCompl K} (c d : V), c ∈ C → d ∉ K → G.Adj c d → d ∈ C :=
  fun {C} c d ⟨cnK, h⟩ dnK cd =>
  ⟨dnK, by
    rw [← h, ConnectedComponent.eq]
    exact Adj.reachable cd.symm⟩

Proof state:
V : Type u
G : SimpleGraph V
K : Set V
C : G.ComponentCompl K
c d : V
x✝ : c ∈ C
dnK : d ∉ K
cd : G.Adj c d
cnK : c ∉ K
h : G.componentComplMk cnK = C
⊢ (induce Kᶜ G).Reachable ⟨d, dnK⟩ ⟨c, cnK⟩

Tactic:
exact Adj.reachable cd.symm

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
K : Set V
C : G.ComponentCompl K
c d : V
x✝ : c ∈ C
dnK : d ∉ K
cd : G.Adj c d
cnK : c ∉ K
h : G.componentComplMk cnK = C
⊢ G.componentComplMk dnK = C

Tactic:
rw [← h, ConnectedComponent.eq]

Result:
V : Type u
G : SimpleGraph V
K : Set V
C : G.ComponentCompl K
c d : V
x✝ : c ∈ C
dnK : d ∉ K
cd : G.Adj c d
cnK : c ∉ K
h : G.componentComplMk cnK = C
⊢ (induce Kᶜ G).Reachable ⟨d, dnK⟩ ⟨c, cnK⟩