harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem isNormal_comap {S : Subgroupoid D} (Sn : IsNormal S) : IsNormal (comap φ S) where
  wide c

Proof state:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
Sn : S.IsNormal
c : C
⊢ 𝟙 (φ.obj c) ∈ S.arrows (φ.obj c) (φ.obj c)

Tactic:
apply Sn.wide

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
Sn : S.IsNormal
c✝ d✝ : C
f : c✝ ⟶ d✝
γ : c✝ ⟶ c✝
hγ : γ ∈ (comap φ S).arrows c✝ c✝
⊢ Groupoid.inv f ≫ γ ≫ f ∈ (comap φ S).arrows d✝ d✝

Tactic:
simp_rw [inv_eq_inv f, comap, mem_setOf, Functor.map_comp, Functor.map_inv, ← inv_eq_inv]

Result:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
Sn : S.IsNormal
c✝ d✝ : C
f : c✝ ⟶ d✝
γ : c✝ ⟶ c✝
hγ : γ ∈ (comap φ S).arrows c✝ c✝
⊢ Groupoid.inv (φ.map f) ≫ φ.map γ ≫ φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj d✝)

Proof state:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
Sn : S.IsNormal
c : C
⊢ 𝟙 c ∈ (comap φ S).arrows c c

Tactic:
rw [comap, mem_setOf, Functor.map_id]

Result:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
Sn : S.IsNormal
c : C
⊢ 𝟙 (φ.obj c) ∈ S.arrows (φ.obj c) (φ.obj c)

Proof state:
C : Type u
inst✝¹ : Groupoid C
D : Type u_1
inst✝ : Groupoid D
φ : C ⥤ D
S : Subgroupoid D
Sn : S.IsNormal
c✝ d✝ : C
f : c✝ ⟶ d✝
γ : c✝ ⟶ c✝
hγ : γ ∈ (comap φ S).arrows c✝ c✝
⊢ Groupoid.inv (φ.map f) ≫ φ.map γ ≫ φ.map f ∈ S.arrows (φ.obj d✝) (φ.obj d✝)

Tactic:
exact Sn.conj _ hγ

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem exists_nat_gt {r : ℝ≥0∞} (h : r ≠ ∞) : ∃ n : ℕ, r < n

Proof state:
case intro.intro
r : ℝ≥0
n : ℕ
hn : r < ↑n
⊢ ∃ n, ↑r < ↑n

Tactic:
exact ⟨n, coe_lt_natCast.2 hn⟩

Result:
no goals

Proof state:
r : ℝ≥0∞
h : r ≠ ⊤
⊢ ∃ n, r < ↑n

Tactic:
lift r to ℝ≥0 using h

Result:
case intro
r : ℝ≥0
⊢ ∃ n, ↑r < ↑n

Proof state:
case intro
r : ℝ≥0
⊢ ∃ n, ↑r < ↑n

Tactic:
rcases exists_nat_gt r with ⟨n, hn⟩

Result:
case intro.intro
r : ℝ≥0
n : ℕ
hn : r < ↑n
⊢ ∃ n, ↑r < ↑n
-- Mathlib/LinearAlgebra/QuadraticForm/Prod.lean
theorem isOrtho_inr_inr_iff {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P}
    (m₂ m₂' : M₂) :
    (Q₁.prod Q₂).IsOrtho (0, m₂) (0, m₂') ↔ Q₂.IsOrtho m₂ m₂'

Proof state:
R : Type u_2
M₁ : Type u_3
M₂ : Type u_4
P : Type u_7
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid P
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R P
Q₁ : QuadraticMap R M₁ P
Q₂ : QuadraticMap R M₂ P
m₂ m₂' : M₂
⊢ (Q₁.prod Q₂).IsOrtho (0, m₂) (0, m₂') ↔ Q₂.IsOrtho m₂ m₂'

Tactic:
simp [isOrtho_def]

Result:
no goals
-- Mathlib/Topology/Connected/Clopen.lean
/-- In a preconnected set, if a symmetric transitive relation `P x y` is true for `y` close
enough to `x`, then it holds for all `x, y`. This is a version of the fact that, if an equivalence
relation has open classes, then it has a single equivalence class. -/
lemma IsPreconnected.induction₂ {s : Set α} (hs : IsPreconnected s) (P : α → α → Prop)
    (h : ∀ x ∈ s, ∀ᶠ y in 𝓝[s] x, P x y)
    (h' : ∀ x y z, x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z)
    (h'' : ∀ x y, x ∈ s → y ∈ s → P x y → P y x)
    {x y : α} (hx : x ∈ s) (hy : y ∈ s) : P x y

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x
x y : α
hx : x ∈ s
hy : y ∈ s
⊢ P x y

Tactic:
apply hs.induction₂' P (fun z hz ↦ ?_) h' hx hy

Result:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x
x y : α
hx : x ∈ s
hy : y ∈ s
z : α
hz : z ∈ s
⊢ ∀ᶠ (y : α) in 𝓝[s] z, P z y ∧ P y z

Proof state:
case h
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x
x y : α
hx : x ∈ s
hy : y ∈ s
z : α
hz : z ∈ s
a : α
ha : P z a
h'a : a ∈ s
⊢ P z a ∧ P a z

Tactic:
exact ⟨ha, h'' z a hz h'a ha⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x
x y : α
hx : x ∈ s
hy : y ∈ s
z : α
hz : z ∈ s
⊢ ∀ᶠ (y : α) in 𝓝[s] z, P z y ∧ P y z

Tactic:
filter_upwards [h z hz, self_mem_nhdsWithin] with a ha h'a

Result:
case h
α : Type u
inst✝ : TopologicalSpace α
s : Set α
hs : IsPreconnected s
P : α → α → Prop
h : ∀ x ∈ s, ∀ᶠ (y : α) in 𝓝[s] x, P x y
h' : ∀ (x y z : α), x ∈ s → y ∈ s → z ∈ s → P x y → P y z → P x z
h'' : ∀ (x y : α), x ∈ s → y ∈ s → P x y → P y x
x y : α
hx : x ∈ s
hy : y ∈ s
z : α
hz : z ∈ s
a : α
ha : P z a
h'a : a ∈ s
⊢ P z a ∧ P a z
-- Mathlib/Algebra/Order/Quantale.lean
theorem mul_bot : x * ⊥ = ⊥

Proof state:
α : Type u_3
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
x : α
⊢ x * ⊥ = ⊥

Tactic:
rw [← sSup_empty, mul_sSup_distrib]

Result:
α : Type u_3
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
x : α
⊢ ⨆ y ∈ ∅, x * y = sSup ∅

Proof state:
α : Type u_3
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
x : α
⊢ ⨆ y ∈ ∅, x * y = sSup ∅

Tactic:
simp only [Set.mem_empty_iff_false, not_false_eq_true, iSup_neg, iSup_bot, sSup_empty]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem ext_getElem?' {l₁ l₂ : List α} (h' : ∀ n < max l₁.length l₂.length, l₁[n]? = l₂[n]?) :
    l₁ = l₂

Proof state:
α : Type u
l₁ l₂ : List α
h' : ∀ (n : ℕ), n < l₁.length ⊔ l₂.length → l₁[n]? = l₂[n]?
⊢ l₁ = l₂

Tactic:
apply ext_getElem?

Result:
case h
α : Type u
l₁ l₂ : List α
h' : ∀ (n : ℕ), n < l₁.length ⊔ l₂.length → l₁[n]? = l₂[n]?
⊢ ∀ (i : ℕ), l₁[i]? = l₂[i]?

Proof state:
case h
α : Type u
l₁ l₂ : List α
h' : ∀ (n : ℕ), n < l₁.length ⊔ l₂.length → l₁[n]? = l₂[n]?
⊢ ∀ (i : ℕ), l₁[i]? = l₂[i]?

Tactic:
intro n

Result:
case h
α : Type u
l₁ l₂ : List α
h' : ∀ (n : ℕ), n < l₁.length ⊔ l₂.length → l₁[n]? = l₂[n]?
n : ℕ
⊢ l₁[n]? = l₂[n]?

Proof state:
case h.inl
α : Type u
l₁ l₂ : List α
h' : ∀ (n : ℕ), n < l₁.length ⊔ l₂.length → l₁[n]? = l₂[n]?
n : ℕ
hn : n < l₁.length ⊔ l₂.length
⊢ l₁[n]? = l₂[n]?

Tactic:
exact h' n hn

Result:
no goals

Proof state:
case h
α : Type u
l₁ l₂ : List α
h' : ∀ (n : ℕ), n < l₁.length ⊔ l₂.length → l₁[n]? = l₂[n]?
n : ℕ
⊢ l₁[n]? = l₂[n]?

Tactic:
rcases Nat.lt_or_ge n <| max l₁.length l₂.length with hn | hn

Result:
case h.inl
α : Type u
l₁ l₂ : List α
h' : ∀ (n : ℕ), n < l₁.length ⊔ l₂.length → l₁[n]? = l₂[n]?
n : ℕ
hn : n < l₁.length ⊔ l₂.length
⊢ l₁[n]? = l₂[n]?

case h.inr
α : Type u
l₁ l₂ : List α
h' : ∀ (n : ℕ), n < l₁.length ⊔ l₂.length → l₁[n]? = l₂[n]?
n : ℕ
hn : n ≥ l₁.length ⊔ l₂.length
⊢ l₁[n]? = l₂[n]?

Proof state:
case h.inr
α : Type u
l₁ l₂ : List α
h' : ∀ (n : ℕ), n < l₁.length ⊔ l₂.length → l₁[n]? = l₂[n]?
n : ℕ
hn : n ≥ l₁.length ⊔ l₂.length
⊢ l₁[n]? = l₂[n]?

Tactic:
simp_all [Nat.max_le, getElem?_eq_none]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Linear.lean
theorem monoidalLinearOfFaithful {D : Type*} [Category D] [Preadditive D] [Linear R D]
    [MonoidalCategory D] [MonoidalPreadditive D] (F : D ⥤ C) [F.Monoidal] [F.Faithful]
    [F.Linear R] : MonoidalLinear R D :=
  { whiskerLeft_smul

Proof state:
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
X Y Z : D
r : R
f : Y ⟶ Z
⊢ X ◁ (r • f) = r • X ◁ f

Tactic:
apply F.map_injective

Result:
case a
R : Type u_1
inst✝¹⁴ : Semiring R
C : Type u_2
inst✝¹³ : Category.{u_5, u_2} C
inst✝¹² : Preadditive C
inst✝¹¹ : Linear R C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : MonoidalPreadditive C
inst✝⁸ : MonoidalLinear R C
D : Type u_3
inst✝⁷ : Category.{u_4, u_3} D
inst✝⁶ : Preadditive D
inst✝⁵ : Linear R D
inst✝⁴ : MonoidalCategory D
inst✝³ : MonoidalPreadditive D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : Functor.Linear R F
X Y Z : D
r : R
f : Y ⟶ Z
⊢ F.map (X ◁ (r • f)) = F.map (r • X ◁ f)
-- Mathlib/RingTheory/MvPowerSeries/Order.lean
theorem order_eq_nat {n : ℕ} :
    f.order = n ↔
      (∃ d, coeff R d f ≠ 0 ∧ degree d = n) ∧ ∀ d, degree d < n → coeff R d f = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
⊢ f.order = ↑n ↔ (∃ d, (coeff R d) f ≠ 0 ∧ d.degree = n) ∧ ∀ (d : σ →₀ ℕ), d.degree < n → (coeff R d) f = 0

Tactic:
simp_rw [degree_eq_weight_one]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
⊢ f.order = ↑n ↔
    (∃ d, (coeff R d) f ≠ 0 ∧ (weight fun x => 1) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight fun x => 1) d < n → (coeff R d) f = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
f : MvPowerSeries σ R
n : ℕ
⊢ f.order = ↑n ↔
    (∃ d, (coeff R d) f ≠ 0 ∧ (weight fun x => 1) d = n) ∧ ∀ (d : σ →₀ ℕ), (weight fun x => 1) d < n → (coeff R d) f = 0

Tactic:
exact weightedOrder_eq_nat _

Result:
no goals
-- Mathlib/Order/RelSeries.lean
@[simp] lemma head_tail (p : RelSeries r) (len_pos : p.length ≠ 0) :
    (p.tail len_pos).head = p 1

Proof state:
case e_a.h
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ 1 < p.length + 1

Tactic:
simpa only [lt_add_iff_pos_left, Nat.pos_iff_ne_zero]

Result:
no goals

Proof state:
case e_a.h
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ ↑(Fin.cast ⋯ 0).succ = ↑1

Tactic:
show (1 : ℕ) = (1 : ℕ) % _

Result:
case e_a.h
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ 1 = 1 % (p.length + 1)

Proof state:
case e_a
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ (Fin.cast ⋯ 0).succ = 1

Tactic:
ext

Result:
case e_a.h
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ ↑(Fin.cast ⋯ 0).succ = ↑1

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ p.toFun (Fin.cast ⋯ 0).succ = p.toFun 1

Tactic:
congr

Result:
case e_a
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ (Fin.cast ⋯ 0).succ = 1

Proof state:
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ (p.tail len_pos).head = p.toFun 1

Tactic:
show p (Fin.succ _) = p 1

Result:
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ p.toFun (Fin.cast ⋯ 0).succ = p.toFun 1

Proof state:
case e_a.h
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ 1 = 1 % (p.length + 1)

Tactic:
rw [Nat.mod_eq_of_lt]

Result:
case e_a.h
α : Type u_1
r : Rel α α
p : RelSeries r
len_pos : p.length ≠ 0
⊢ 1 < p.length + 1
-- Mathlib/Computability/Language.lean
theorem one_add_self_mul_kstar_eq_kstar (l : Language α) : 1 + l * l∗ = l∗

Proof state:
α : Type u_1
l : Language α
⊢ 1 + l * l∗ = l∗

Tactic:
simp only [kstar_eq_iSup_pow, mul_iSup, ← pow_succ', ← pow_zero l]

Result:
α : Type u_1
l : Language α
⊢ l ^ 0 + ⨆ i, l ^ (i + 1) = ⨆ i, l ^ i

Proof state:
α : Type u_1
l : Language α
⊢ l ^ 0 + ⨆ i, l ^ (i + 1) = ⨆ i, l ^ i

Tactic:
exact sup_iSup_nat_succ _

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem le_limsup_of_frequently_le {α β} [ConditionallyCompleteLinearOrder β] {f : Filter α}
    {u : α → β} {b : β} (hu_le : ∃ᶠ x in f, b ≤ u x)
    (hu : f.IsBoundedUnder (· ≤ ·) u

Proof state:
α : Type u_6
β : Type u_7
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu_le : ∃ᶠ (x : α) in f, b ≤ u x
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
⊢ b ≤ limsup u f

Tactic:
revert hu_le

Result:
α : Type u_6
β : Type u_7
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
⊢ (∃ᶠ (x : α) in f, b ≤ u x) → b ≤ limsup u f

Proof state:
α : Type u_6
β : Type u_7
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
⊢ (∃ᶠ (x : α) in f, b ≤ u x) → b ≤ limsup u f

Tactic:
rw [← not_imp_not, not_frequently]

Result:
α : Type u_6
β : Type u_7
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
⊢ ¬b ≤ limsup u f → ∀ᶠ (x : α) in f, ¬b ≤ u x

Proof state:
α : Type u_6
β : Type u_7
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
⊢ limsup u f < b → ∀ᶠ (x : α) in f, u x < b

Tactic:
exact fun h => eventually_lt_of_limsup_lt h hu

Result:
no goals

Proof state:
α : Type u_6
β : Type u_7
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
⊢ ¬b ≤ limsup u f → ∀ᶠ (x : α) in f, ¬b ≤ u x

Tactic:
simp_rw [← lt_iff_not_ge]

Result:
α : Type u_6
β : Type u_7
inst✝ : ConditionallyCompleteLinearOrder β
f : Filter α
u : α → β
b : β
hu : autoParam (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) _auto✝
⊢ limsup u f < b → ∀ᶠ (x : α) in f, u x < b
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem prod_mul_reverse_inv_prod (L : List (TransvectionStruct n R)) :
    (L.map toMatrix).prod * (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod = 1

Proof state:
case nil
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
⊢ (List.map toMatrix []).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) [].reverse).prod = 1

Tactic:
simp

Result:
no goals

Proof state:
case cons
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod = 1
⊢ (List.map toMatrix (t :: L)).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) (t :: L).reverse).prod = 1

Tactic:
suffices
  t.toMatrix *
        ((L.map toMatrix).prod * (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod) *
      t.inv.toMatrix = 1
  by simpa [Matrix.mul_assoc]

Result:
case cons
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod = 1
⊢ t.toMatrix * ((List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod) *
      t.inv.toMatrix =
    1

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
L : List (TransvectionStruct n R)
⊢ (List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod = 1

Tactic:
induction L with
| nil => simp
| cons t L IH =>
  suffices
    t.toMatrix *
          ((L.map toMatrix).prod * (L.reverse.map (toMatrix ∘ TransvectionStruct.inv)).prod) *
        t.inv.toMatrix = 1
    by simpa [Matrix.mul_assoc]
  simp_rw [IH, Matrix.mul_one, t.mul_inv]

Result:
no goals

Proof state:
case cons
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod = 1
⊢ t.toMatrix * ((List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod) *
      t.inv.toMatrix =
    1

Tactic:
simp_rw [IH, Matrix.mul_one, t.mul_inv]

Result:
no goals

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
inst✝ : Fintype n
t : TransvectionStruct n R
L : List (TransvectionStruct n R)
IH : (List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod = 1
this :
  t.toMatrix * ((List.map toMatrix L).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) L.reverse).prod) *
      t.inv.toMatrix =
    1
⊢ (List.map toMatrix (t :: L)).prod * (List.map (toMatrix ∘ TransvectionStruct.inv) (t :: L).reverse).prod = 1

Tactic:
simpa [Matrix.mul_assoc]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem filterRevM_toArray [Monad m] [LawfulMonad m] (l : List α) (p : α → m Bool) :
    l.toArray.filterRevM p = toArray <$> l.filterRevM p

Proof state:
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
p : α → m Bool
⊢ Array.filterRevM p l.toArray = toArray <$> filterRevM p l

Tactic:
simp [Array.filterRevM, filterRevM]

Result:
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
p : α → m Bool
⊢ Array.reverse <$>
      foldrM
        (fun x y => do
          let __do_lift ← p x
          if __do_lift = true then pure (y.push x) else pure y)
        #[] l =
    toArray <$> filterAuxM p l.reverse []

Proof state:
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
p : α → m Bool
⊢ Array.reverse <$> toArray <$> filterM p l.reverse = toArray <$> filterAuxM p l.reverse []

Tactic:
simp only [filterM, bind_pure_comp, Functor.map_map, reverse_toArray, reverse_reverse]

Result:
no goals

Proof state:
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
p : α → m Bool
⊢ Array.reverse <$>
      foldrM
        (fun x y => do
          let __do_lift ← p x
          if __do_lift = true then pure (y.push x) else pure y)
        #[] l =
    toArray <$> filterAuxM p l.reverse []

Tactic:
rw [← foldlM_reverse, ← foldlM_toArray, ← Array.filterM, filterM_toArray]

Result:
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
l : List α
p : α → m Bool
⊢ Array.reverse <$> toArray <$> filterM p l.reverse = toArray <$> filterAuxM p l.reverse []
-- Mathlib/Algebra/Quaternion.lean
theorem self_add_star' : a + star a = ↑(2 * a.re + c₂ * a.imI)

Proof state:
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ a + star a = ↑(2 * a.re + c₂ * a.imI)

Tactic:
ext <;> simp [two_mul]

Result:
case re
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ a.re + (a.re + c₂ * a.imI) = a.re + a.re + c₂ * a.imI

Proof state:
case re
R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ a.re + (a.re + c₂ * a.imI) = a.re + a.re + c₂ * a.imI

Tactic:
ring

Result:
no goals
-- Mathlib/Topology/Bornology/Absorbs.lean
@[simp]
lemma absorbs_inter : Absorbs G₀ (s ∩ t) u ↔ Absorbs G₀ s u ∧ Absorbs G₀ t u

Proof state:
G₀ : Type u_1
α : Type u_2
inst✝² : GroupWithZero G₀
inst✝¹ : Bornology G₀
inst✝ : MulAction G₀ α
s t u : Set α
⊢ Absorbs G₀ (s ∩ t) u ↔ Absorbs G₀ s u ∧ Absorbs G₀ t u

Tactic:
simp only [absorbs_iff_eventually_cobounded_mapsTo, mapsTo_inter, eventually_and]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Polynomial.lean
theorem polynomialFunctions.starClosure_le_equalizer {A : Type*} [StarRing R] [ContinuousStar R]
    [Semiring A] [StarRing A] [Algebra R A] (s : Set R) (φ ψ : C(s, R) →⋆ₐ[R] A)
    (h : φ (toContinuousMapOnAlgHom s X) = ψ (toContinuousMapOnAlgHom s X)) :
    (polynomialFunctions s).starClosure ≤ StarAlgHom.equalizer φ ψ

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : IsTopologicalSemiring R
A : Type u_2
inst✝⁴ : StarRing R
inst✝³ : ContinuousStar R
inst✝² : Semiring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
s : Set R
φ ψ : C(↑s, R) →⋆ₐ[R] A
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ adjoin R {(toContinuousMapOnAlgHom s) X} ≤ StarAlgHom.equalizer φ ψ

Tactic:
exact StarAlgHom.adjoin_le_equalizer φ ψ fun x hx => (Set.mem_singleton_iff.1 hx).symm ▸ h

Result:
no goals

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : IsTopologicalSemiring R
A : Type u_2
inst✝⁴ : StarRing R
inst✝³ : ContinuousStar R
inst✝² : Semiring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
s : Set R
φ ψ : C(↑s, R) →⋆ₐ[R] A
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ (polynomialFunctions s).starClosure ≤ StarAlgHom.equalizer φ ψ

Tactic:
rw [polynomialFunctions.starClosure_eq_adjoin_X s]

Result:
R : Type u_1
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : IsTopologicalSemiring R
A : Type u_2
inst✝⁴ : StarRing R
inst✝³ : ContinuousStar R
inst✝² : Semiring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
s : Set R
φ ψ : C(↑s, R) →⋆ₐ[R] A
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ adjoin R {(toContinuousMapOnAlgHom s) X} ≤ StarAlgHom.equalizer φ ψ
-- Mathlib/Data/Multiset/Bind.lean
theorem cons_sigma : (a ::ₘ s).sigma t = (t a).map (Sigma.mk a) + s.sigma t

Proof state:
α : Type u_1
σ : α → Type u_4
a : α
s : Multiset α
t : (a : α) → Multiset (σ a)
⊢ (a ::ₘ s).sigma t = map (Sigma.mk a) (t a) + s.sigma t

Tactic:
simp [Multiset.sigma]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_zero : (0#w).getMsbD i = false

Proof state:
w i : Nat
⊢ (0#w).getMsbD i = false

Tactic:
simp [getMsbD]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
theorem eLpNorm_le_eLpNorm_of_exponent_le {p q : ℝ≥0∞} (hpq : p ≤ q) [IsProbabilityMeasure μ]
    (hf : AEStronglyMeasurable f μ) : eLpNorm f p μ ≤ eLpNorm f q μ :=
  (eLpNorm_le_eLpNorm_mul_rpow_measure_univ hpq hf).trans (le_of_eq (by simp [measure_univ]))

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
μ : Measure α
f : α → E
p q : ℝ≥0∞
hpq : p ≤ q
inst✝ : IsProbabilityMeasure μ
hf : AEStronglyMeasurable f μ
⊢ eLpNorm f q μ * μ Set.univ ^ (1 / p.toReal - 1 / q.toReal) = eLpNorm f q μ

Tactic:
simp [measure_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem pop_range' : (range' s n step).pop = range' s (n - 1) step

Proof state:
s n step : Nat
⊢ (range' s n step).pop = range' s (n - 1) step

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem last_le_iff {n : Nat} {k : Fin (n + 1)} : last n ≤ k ↔ k = last n

Proof state:
n : Nat
k : Fin (n + 1)
⊢ last n ≤ k ↔ k = last n

Tactic:
rw [Fin.ext_iff, Nat.le_antisymm_iff, le_def, and_iff_right (by apply le_last)]

Result:
no goals

Proof state:
n : Nat
k : Fin (n + 1)
⊢ ↑k ≤ ↑(last n)

Tactic:
apply le_last

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/Comp.lean
theorem comp_null (a : α) (hs : MeasurableSet s) :
    (η ∘ₖ κ) a s = 0 ↔ (fun y ↦ η y s) =ᵐ[κ a] 0

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
η : Kernel β γ
s : Set γ
a : α
hs : MeasurableSet s
⊢ ((η ∘ₖ κ) a) s = 0 ↔ (fun y => (η y) s) =ᶠ[ae (κ a)] 0

Tactic:
rw [comp_apply' _ _ _ hs, lintegral_eq_zero_iff (η.measurable_coe hs)]

Result:
no goals
-- Mathlib/FieldTheory/Galois/GaloisClosure.lean
theorem adjoin_simple_le_iff [IsGalois k K] {x : K} {L : FiniteGaloisIntermediateField k K} :
    adjoin k {x} ≤ L ↔ x ∈ L.toIntermediateField

Proof state:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
x : K
L : FiniteGaloisIntermediateField k K
⊢ adjoin k {x} ≤ L ↔ x ∈ L.toIntermediateField

Tactic:
simp only [le_iff, adjoin_val, IntermediateField.normalClosure_le_iff_of_normal,
  IntermediateField.adjoin_le_iff, Set.le_eq_subset, Set.singleton_subset_iff, SetLike.mem_coe]

Result:
no goals