harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Log/PosLog.lean
theorem posLog_prod {α : Type*} (s : Finset α) (f : α → ℝ) :
    log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)

Proof state:
α : Type u_1
s✝ : Finset α
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
⊢ log⁺ (∏ t ∈ insert a s, f t) = log⁺ (f a * ∏ t ∈ s, f t)

Tactic:
rw [Finset.prod_insert ha]

Result:
no goals

Proof state:
case insert
α : Type u_1
s : Finset α
f : α → ℝ
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    a ∉ s → log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t) → log⁺ (∏ t ∈ insert a s, f t) ≤ ∑ t ∈ insert a s, log⁺ (f t)

Tactic:
intro a s ha hs

Result:
case insert
α : Type u_1
s✝ : Finset α
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
⊢ log⁺ (∏ t ∈ insert a s, f t) ≤ ∑ t ∈ insert a s, log⁺ (f t)

Proof state:
case empty
α : Type u_1
s : Finset α
f : α → ℝ
⊢ log⁺ (∏ t ∈ ∅, f t) ≤ ∑ t ∈ ∅, log⁺ (f t)

Tactic:
simp [posLog]

Result:
no goals

Proof state:
case insert
α : Type u_1
s✝ : Finset α
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
⊢ log⁺ (∏ t ∈ insert a s, f t) ≤ ∑ t ∈ insert a s, log⁺ (f t)

Tactic:
calc log⁺ (∏ t ∈ insert a s, f t)
_ = log⁺ (f a * ∏ t ∈ s, f t) := by rw [Finset.prod_insert ha]
_ ≤ log⁺ (f a) + log⁺ (∏ t ∈ s, f t) := posLog_mul
_ ≤ log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) := add_le_add (by rfl) hs
_ = ∑ t ∈ insert a s, log⁺ (f t) := by rw [Finset.sum_insert ha]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ
⊢ log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)

Tactic:
apply Finset.induction (p := fun (S : Finset α) ↦ (log⁺ (∏ t ∈ S, f t) ≤ ∑ t ∈ S, log⁺ (f t)))

Result:
case empty
α : Type u_1
s : Finset α
f : α → ℝ
⊢ log⁺ (∏ t ∈ ∅, f t) ≤ ∑ t ∈ ∅, log⁺ (f t)

case insert
α : Type u_1
s : Finset α
f : α → ℝ
⊢ ∀ ⦃a : α⦄ {s : Finset α},
    a ∉ s → log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t) → log⁺ (∏ t ∈ insert a s, f t) ≤ ∑ t ∈ insert a s, log⁺ (f t)

Proof state:
α : Type u_1
s✝ : Finset α
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
⊢ log⁺ (f a) ≤ log⁺ (f a)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
s✝ : Finset α
f : α → ℝ
a : α
s : Finset α
ha : a ∉ s
hs : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t)
⊢ log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) = ∑ t ∈ insert a s, log⁺ (f t)

Tactic:
rw [Finset.sum_insert ha]

Result:
no goals
-- Mathlib/Data/Finmap.lean
@[simp] lemma sigma_keys_lookup (s : Finmap β) :
    s.keys.sigma (fun i => (s.lookup i).toFinset) = ⟨s.entries, s.nodup_entries⟩

Proof state:
case h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : (i : α) × β i
this : x ∈ s.entries → x.fst ∈ s.keys
⊢ (x ∈ s.keys.sigma fun i => (lookup i s).toFinset) ↔ x ∈ { val := s.entries, nodup := ⋯ }

Tactic:
simpa [lookup_eq_some_iff]

Result:
no goals

Proof state:
case h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : (i : α) × β i
⊢ (x ∈ s.keys.sigma fun i => (lookup i s).toFinset) ↔ x ∈ { val := s.entries, nodup := ⋯ }

Tactic:
have : x ∈ s.entries → x.1 ∈ s.keys := Multiset.mem_map_of_mem _

Result:
case h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : (i : α) × β i
this : x ∈ s.entries → x.fst ∈ s.keys
⊢ (x ∈ s.keys.sigma fun i => (lookup i s).toFinset) ↔ x ∈ { val := s.entries, nodup := ⋯ }

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
⊢ (s.keys.sigma fun i => (lookup i s).toFinset) = { val := s.entries, nodup := ⋯ }

Tactic:
ext x

Result:
case h
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s : Finmap β
x : (i : α) × β i
⊢ (x ∈ s.keys.sigma fun i => (lookup i s).toFinset) ↔ x ∈ { val := s.entries, nodup := ⋯ }
-- Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean
theorem detp_smul_add_adjp (hAB : A * B = 1) :
    detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
key : adjp 1 B + detp (-1) B • A = adjp (-1) B + detp 1 B • A
⊢ detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B

Tactic:
rwa [add_comm, eq_comm, add_comm]

Result:
no goals

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
key : A * (B * adjp 1 B + detp (-1) B • 1) = A * (B * adjp (-1) B + detp 1 B • 1)
⊢ detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B

Tactic:
simp_rw [mul_add, ← mul_assoc, hAB, one_mul, mul_smul, mul_one] at key

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
key : adjp 1 B + detp (-1) B • A = adjp (-1) B + detp 1 B • A
⊢ detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B

Proof state:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
⊢ detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B

Tactic:
have key := congr(A * $(mul_adjp_add_detp B))

Result:
n : Type u_1
R : Type u_3
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommSemiring R
A B : Matrix n n R
hAB : A * B = 1
key : A * (B * adjp 1 B + detp (-1) B • 1) = A * (B * adjp (-1) B + detp 1 B • 1)
⊢ detp 1 B • A + adjp (-1) B = detp (-1) B • A + adjp 1 B
-- Mathlib/Topology/Basic.lean
theorem IsOpen.union (h₁ : IsOpen s₁) (h₂ : IsOpen s₂) : IsOpen (s₁ ∪ s₂)

Proof state:
X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsOpen s₁
h₂ : IsOpen s₂
⊢ IsOpen (⋃ b, bif b then s₁ else s₂)

Tactic:
exact isOpen_iUnion (Bool.forall_bool.2 ⟨h₂, h₁⟩)

Result:
no goals

Proof state:
X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsOpen s₁
h₂ : IsOpen s₂
⊢ IsOpen (s₁ ∪ s₂)

Tactic:
rw [union_eq_iUnion]

Result:
X : Type u
s₁ s₂ : Set X
inst✝ : TopologicalSpace X
h₁ : IsOpen s₁
h₂ : IsOpen s₂
⊢ IsOpen (⋃ b, bif b then s₁ else s₂)
-- Mathlib/Analysis/Convolution.lean
theorem convolution_smul [SMulCommClass ℝ 𝕜 F] {y : 𝕜} : f ⋆[L, μ] y • g = y • (f ⋆[L, μ] g)

Proof state:
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 E'
inst✝⁴ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : NormedSpace ℝ F
inst✝¹ : AddGroup G
inst✝ : SMulCommClass ℝ 𝕜 F
y : 𝕜
⊢ f ⋆[L, μ] y • g = y • (f ⋆[L, μ] g)

Tactic:
ext

Result:
case h
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 E'
inst✝⁴ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : NormedSpace ℝ F
inst✝¹ : AddGroup G
inst✝ : SMulCommClass ℝ 𝕜 F
y : 𝕜
x✝ : G
⊢ (f ⋆[L, μ] y • g) x✝ = (y • (f ⋆[L, μ] g)) x✝

Proof state:
case h
𝕜 : Type u𝕜
G : Type uG
E : Type uE
E' : Type uE'
F : Type uF
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedAddCommGroup E'
inst✝⁸ : NormedAddCommGroup F
f : G → E
g : G → E'
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 E'
inst✝⁴ : NormedSpace 𝕜 F
L : E →L[𝕜] E' →L[𝕜] F
inst✝³ : MeasurableSpace G
μ : Measure G
inst✝² : NormedSpace ℝ F
inst✝¹ : AddGroup G
inst✝ : SMulCommClass ℝ 𝕜 F
y : 𝕜
x✝ : G
⊢ (f ⋆[L, μ] y • g) x✝ = (y • (f ⋆[L, μ] g)) x✝

Tactic:
simp only [Pi.smul_apply, convolution_def, ← integral_smul, (L _).map_smul]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
protected lemma sum_div (hf : ∀ i ∈ s, n ∣ f i) : (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n

Proof state:
case inr
ι : Type u_7
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
hn : n > 0
⊢ ∑ i ∈ s, f i = ∑ i ∈ s, f i / n * n

Tactic:
refine sum_congr rfl fun s hs ↦ ?_

Result:
case inr
ι : Type u_7
s✝ : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s✝, n ∣ f i
hn : n > 0
s : ι
hs : s ∈ s✝
⊢ f s = f s / n * n

Proof state:
case inr
ι : Type u_7
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
hn : n > 0
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n

Tactic:
rw [Nat.div_eq_iff_eq_mul_left hn (dvd_sum hf), sum_mul]

Result:
case inr
ι : Type u_7
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
hn : n > 0
⊢ ∑ i ∈ s, f i = ∑ i ∈ s, f i / n * n

Proof state:
ι : Type u_7
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n

Tactic:
obtain rfl | hn := n.eq_zero_or_pos

Result:
case inl
ι : Type u_7
s : Finset ι
f : ι → ℕ
hf : ∀ i ∈ s, 0 ∣ f i
⊢ (∑ i ∈ s, f i) / 0 = ∑ i ∈ s, f i / 0

case inr
ι : Type u_7
s : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s, n ∣ f i
hn : n > 0
⊢ (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n

Proof state:
case inl
ι : Type u_7
s : Finset ι
f : ι → ℕ
hf : ∀ i ∈ s, 0 ∣ f i
⊢ (∑ i ∈ s, f i) / 0 = ∑ i ∈ s, f i / 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
ι : Type u_7
s✝ : Finset ι
f : ι → ℕ
n : ℕ
hf : ∀ i ∈ s✝, n ∣ f i
hn : n > 0
s : ι
hs : s ∈ s✝
⊢ f s = f s / n * n

Tactic:
rw [Nat.div_mul_cancel (hf _ hs)]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrderIso.lean
theorem preimage_Iic (e : α ≃o β) (b : β) : e ⁻¹' Iic b = Iic (e.symm b)

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
x : α
⊢ x ∈ ⇑e ⁻¹' Iic b ↔ x ∈ Iic (e.symm b)

Tactic:
simp [← e.le_iff_le]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
⊢ ⇑e ⁻¹' Iic b = Iic (e.symm b)

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
b : β
x : α
⊢ x ∈ ⇑e ⁻¹' Iic b ↔ x ∈ Iic (e.symm b)
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem nfpFamily_lt_ord_of_isRegular {ι} {f : ι → Ordinal → Ordinal} {c} (hc : IsRegular c)
    (hι : #ι < c) (hc' : c ≠ ℵ₀) {a} (hf : ∀ (i), ∀ b < c.ord, f i b < c.ord) :
    a < c.ord → nfpFamily.{u, u} f a < c.ord :=
  nfpFamily_lt_ord_lift_of_isRegular hc (by rwa [lift_id]) hc' hf

Proof state:
ι : Type u
f : ι → Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
hc' : c ≠ ℵ₀
a : Ordinal.{u}
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
⊢ lift.{?u.133845, u} #ι < c

Tactic:
rwa [lift_id]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Multiset.lean
lemma map_add_right_Icc (a b c : α) : ((Icc a b).map fun x => x + c) = Icc (a + c) (b + c)

Proof state:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Icc a b) = Icc (c + a) (c + b)

Tactic:
exact map_add_left_Icc _ _ _

Result:
no goals

Proof state:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => x + c) (Icc a b) = Icc (a + c) (b + c)

Tactic:
simp_rw [add_comm _ c]

Result:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Icc a b) = Icc (c + a) (c + b)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getThenInsertIfNew?_snd (h : m.WF) {k : α} {v : β} :
    (getThenInsertIfNew? m k v).2 = m.insertIfNew k v

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw α fun x => β
h : m.WF
k : α
v : β
⊢ (getThenInsertIfNew? m k v).snd = m.insertIfNew k v

Tactic:
simp_to_raw using congrArg Subtype.val (Raw₀.Const.getThenInsertIfNew?_snd _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem head_zipWith {f : α → β → γ} (h):
    (List.zipWith f as bs).head h = f (as.head (by rintro rfl; simp_all)) (bs.head (by rintro rfl; simp_all))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
h : zipWith f as bs ≠ []
⊢ (zipWith f as bs).head h = f (as.head ⋯) (bs.head ⋯)

Tactic:
apply Option.some.inj

Result:
case x
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
h : zipWith f as bs ≠ []
⊢ some ((zipWith f as bs).head h) = some (f (as.head ⋯) (bs.head ⋯))

Proof state:
α : Type ?u.35201
β : Type ?u.35200
γ : Type ?u.35199
as : List α
bs : List β
f : α → β → γ
h : zipWith f as bs ≠ []
⊢ as ≠ []

Tactic:
rintro rfl

Result:
α : Type ?u.35201
β : Type ?u.35200
γ : Type ?u.35199
bs : List β
f : α → β → γ
h : zipWith f [] bs ≠ []
⊢ False

Proof state:
α : Type ?u.35201
β : Type ?u.35200
γ : Type ?u.35199
as : List α
bs : List β
f : α → β → γ
h : zipWith f as bs ≠ []
⊢ bs ≠ []

Tactic:
rintro rfl

Result:
α : Type ?u.35201
β : Type ?u.35200
γ : Type ?u.35199
as : List α
f : α → β → γ
h : zipWith f as [] ≠ []
⊢ False

Proof state:
case x
α : Type u_1
β : Type u_2
γ : Type u_3
as : List α
bs : List β
f : α → β → γ
h : zipWith f as bs ≠ []
⊢ some ((zipWith f as bs).head h) = some (f (as.head ⋯) (bs.head ⋯))

Tactic:
rw [← head?_eq_head, head?_zipWith, head?_eq_head, head?_eq_head]

Result:
no goals

Proof state:
α : Type ?u.35201
β : Type ?u.35200
γ : Type ?u.35199
as : List α
f : α → β → γ
h : zipWith f as [] ≠ []
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type ?u.35201
β : Type ?u.35200
γ : Type ?u.35199
bs : List β
f : α → β → γ
h : zipWith f [] bs ≠ []
⊢ False

Tactic:
simp_all

Result:
no goals
-- Mathlib/AlgebraicGeometry/Gluing.lean
theorem gluedCoverT'_snd_snd (x y z : 𝒰.J) :
    gluedCoverT' 𝒰 x y z ≫ pullback.snd _ _ ≫ pullback.snd _ _ =
      pullback.fst _ _ ≫ pullback.fst _ _

Proof state:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ ((pullbackRightPullbackFstIso (𝒰.map x) (𝒰.map z) (pullback.fst (𝒰.map x) (𝒰.map y))).hom ≫
        (pullback.map (pullback.fst (𝒰.map x) (𝒰.map y) ≫ 𝒰.map x) (𝒰.map z)
              (pullback.fst (𝒰.map y) (𝒰.map x) ≫ 𝒰.map y) (𝒰.map z) (pullbackSymmetry (𝒰.map x) (𝒰.map y)).hom
              (𝟙 (𝒰.obj z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.map y) (𝒰.map z) (pullback.fst (𝒰.map y) (𝒰.map x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.map y) (𝒰.map x)) (pullback.fst (𝒰.map y) (𝒰.map z))).hom) ≫
      pullback.snd (pullback.fst (𝒰.map y) (𝒰.map z)) (pullback.fst (𝒰.map y) (𝒰.map x)) ≫
        pullback.snd (𝒰.map y) (𝒰.map x) =
    pullback.fst (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) ≫
      pullback.fst (𝒰.map x) (𝒰.map y)

Tactic:
simp

Result:
no goals

Proof state:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ gluedCoverT' 𝒰 x y z ≫
      pullback.snd (pullback.fst (𝒰.map y) (𝒰.map z)) (pullback.fst (𝒰.map y) (𝒰.map x)) ≫
        pullback.snd (𝒰.map y) (𝒰.map x) =
    pullback.fst (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) ≫
      pullback.fst (𝒰.map x) (𝒰.map y)

Tactic:
delta gluedCoverT'

Result:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.J
⊢ ((pullbackRightPullbackFstIso (𝒰.map x) (𝒰.map z) (pullback.fst (𝒰.map x) (𝒰.map y))).hom ≫
        (pullback.map (pullback.fst (𝒰.map x) (𝒰.map y) ≫ 𝒰.map x) (𝒰.map z)
              (pullback.fst (𝒰.map y) (𝒰.map x) ≫ 𝒰.map y) (𝒰.map z) (pullbackSymmetry (𝒰.map x) (𝒰.map y)).hom
              (𝟙 (𝒰.obj z)) (𝟙 X) ⋯ ⋯ ≫
            (pullbackRightPullbackFstIso (𝒰.map y) (𝒰.map z) (pullback.fst (𝒰.map y) (𝒰.map x))).inv) ≫
          (pullbackSymmetry (pullback.fst (𝒰.map y) (𝒰.map x)) (pullback.fst (𝒰.map y) (𝒰.map z))).hom) ≫
      pullback.snd (pullback.fst (𝒰.map y) (𝒰.map z)) (pullback.fst (𝒰.map y) (𝒰.map x)) ≫
        pullback.snd (𝒰.map y) (𝒰.map x) =
    pullback.fst (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) ≫
      pullback.fst (𝒰.map x) (𝒰.map y)
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem eval_nodal_not_at_node [Nontrivial R] [NoZeroDivisors R] {x : R}
    (hx : ∀ i ∈ s, x ≠ v i) : eval x (nodal s v) ≠ 0

Proof state:
R : Type u_1
inst✝² : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
x : R
hx : ∀ i ∈ s, x ≠ v i
⊢ ∀ a ∈ s, x ≠ v a

Tactic:
exact hx

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
x : R
hx : ∀ i ∈ s, x ≠ v i
⊢ eval x (nodal s v) ≠ 0

Tactic:
simp_rw [nodal, eval_prod, prod_ne_zero_iff, eval_sub, eval_X, eval_C, sub_ne_zero]

Result:
R : Type u_1
inst✝² : CommRing R
ι : Type u_2
s : Finset ι
v : ι → R
inst✝¹ : Nontrivial R
inst✝ : NoZeroDivisors R
x : R
hx : ∀ i ∈ s, x ≠ v i
⊢ ∀ a ∈ s, x ≠ v a
-- Mathlib/Computability/Partrec.lean
theorem cond {c : α → Bool} {f : α → σ} {g : α → σ} (hc : Computable c) (hf : Computable f)
    (hg : Computable g) : Computable fun a => cond (c a) (f a) (g a) :=
  (nat_casesOn (encode_iff.2 hc) hg (hf.comp fst).to₂).of_eq fun a => by cases c a <;> rfl

Proof state:
α : Type u_1
σ : Type u_4
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
c : α → Bool
f g : α → σ
hc : Computable c
hf : Computable f
hg : Computable g
a : α
⊢ (Nat.casesOn (encode (c a)) (g a) fun b => f (a, b).1) = bif c a then f a else g a

Tactic:
cases c a <;> rfl

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem mul : Nat.Primrec (unpaired (· * ·)) :=
  (prec zero (add.comp (pair left (right.comp right)))).of_eq fun p => by
    simp; induction p.unpair.2 <;> simp [*, mul_succ, add_comm _ (unpair p).fst]

Proof state:
p : ℕ
⊢ Nat.rec 0 (fun y IH => (unpair p).1 + IH) (unpair p).2 = (unpair p).1 * (unpair p).2

Tactic:
induction p.unpair.2 <;> simp [*, mul_succ, add_comm _ (unpair p).fst]

Result:
no goals

Proof state:
p : ℕ
⊢ unpaired
      (fun z n =>
        Nat.rec 0
          (fun y IH =>
            unpaired (fun x1 x2 => x1 + x2)
              (Nat.pair (unpair (Nat.pair z (Nat.pair y IH))).1 (unpair (unpair (Nat.pair z (Nat.pair y IH))).2).2))
          n)
      p =
    unpaired (fun x1 x2 => x1 * x2) p

Tactic:
simp

Result:
p : ℕ
⊢ Nat.rec 0 (fun y IH => (unpair p).1 + IH) (unpair p).2 = (unpair p).1 * (unpair p).2
-- Mathlib/CategoryTheory/Endofunctor/Algebra.lean
theorem left_inv' :
    ⟨strInv h ≫ A.str, by rw [← Category.assoc, F.map_comp, strInv, ← Hom.h]⟩ = 𝟙 A :=
  Limits.IsInitial.hom_ext h _ (𝟙 A)

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ C
A✝ A₀ A₁ A₂ : Algebra F
f : A₀ ⟶ A₁
g : A₁ ⟶ A₂
A : Algebra F
h : Limits.IsInitial A
⊢ F.map (strInv h ≫ A.str) ≫ A.str = A.str ≫ strInv h ≫ A.str

Tactic:
rw [← Category.assoc, F.map_comp, strInv, ← Hom.h]

Result:
no goals
-- Mathlib/Data/Multiset/NatAntidiagonal.lean
theorem map_swap_antidiagonal {n : ℕ} : (antidiagonal n).map Prod.swap = antidiagonal n

Proof state:
n : ℕ
⊢ map Prod.swap (antidiagonal n) = antidiagonal n

Tactic:
rw [antidiagonal, map_coe, List.Nat.map_swap_antidiagonal, coe_reverse]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem image_eq_iUnion (f : α → β) (s : Set α) : f '' s = ⋃ i ∈ s, {f i} :=
  Set.ext fun b => by simp [@eq_comm β b]

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set α
b : β
⊢ b ∈ f '' s ↔ b ∈ ⋃ i ∈ s, {f i}

Tactic:
simp [@eq_comm β b]

Result:
no goals
-- Mathlib/Data/List/Destutter.lean
theorem destutter'_of_chain (h : l.Chain R a) : l.destutter' R a = a :: l

Proof state:
case cons.intro
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hb : ∀ {a : α}, Chain R a l → destutter' R a l = a :: l
a : α
h✝ : Chain R a (b :: l)
h : R a b
hc : Chain R b l
⊢ destutter' R a (b :: l) = a :: b :: l

Tactic:
rw [l.destutter'_cons_pos h, hb hc]

Result:
no goals

Proof state:
case nil
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
a : α
h : Chain R a []
⊢ destutter' R a [] = [a]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
R : α → α → Prop
inst✝ : DecidableRel R
a : α
h : Chain R a l
⊢ destutter' R a l = a :: l

Tactic:
induction' l with b l hb generalizing a

Result:
case nil
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
a : α
h : Chain R a []
⊢ destutter' R a [] = [a]

case cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hb : ∀ {a : α}, Chain R a l → destutter' R a l = a :: l
a : α
h : Chain R a (b :: l)
⊢ destutter' R a (b :: l) = a :: b :: l

Proof state:
case cons
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hb : ∀ {a : α}, Chain R a l → destutter' R a l = a :: l
a : α
h : Chain R a (b :: l)
⊢ destutter' R a (b :: l) = a :: b :: l

Tactic:
obtain ⟨h, hc⟩ := chain_cons.mp h

Result:
case cons.intro
α : Type u_1
R : α → α → Prop
inst✝ : DecidableRel R
b : α
l : List α
hb : ∀ {a : α}, Chain R a l → destutter' R a l = a :: l
a : α
h✝ : Chain R a (b :: l)
h : R a b
hc : Chain R b l
⊢ destutter' R a (b :: l) = a :: b :: l
-- Mathlib/Data/Nat/Cast/Order/Basic.lean
theorem cast_pos' {n : ℕ} : (0 : α) < n ↔ 0 < n

Proof state:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 0 < ↑n ↔ 0 < n

Tactic:
cases n <;> simp [cast_add_one_pos]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem lowerBound?_of_some {t : RBNode α} : ∃ x, t.lowerBound? cut (some y) = some x

Proof state:
α : Type u_1
cut : α → Ordering
y : α
t : RBNode α
⊢ ∃ x, lowerBound? cut t (some y) = some x

Tactic:
rw [← reverse_reverse t, lowerBound?_reverse]

Result:
α : Type u_1
cut : α → Ordering
y : α
t : RBNode α
⊢ ∃ x, upperBound? (fun x => (cut x).swap) t.reverse (some y) = some x

Proof state:
α : Type u_1
cut : α → Ordering
y : α
t : RBNode α
⊢ ∃ x, upperBound? (fun x => (cut x).swap) t.reverse (some y) = some x

Tactic:
exact upperBound?_of_some

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/EvenEquiv.lean
theorem e0_mul_e0 : e0 Q * e0 Q = -1 :=
  (ι_sq_scalar _ _).trans <| by simp

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
⊢ (algebraMap R (CliffordAlgebra (Q' Q))) ((Q' Q) (0, 1)) = -1

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Order/Compact.lean
theorem le_sSup_image_Icc (h : ContinuousOn f <| Icc a b) (hc : c ∈ Icc a b) :
    f c ≤ sSup (f '' Icc a b)

Proof state:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
⊢ f c ≤ sSup (f '' Icc a b)

Tactic:
have := mem_image_of_mem f hc

Result:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ f '' Icc a b
⊢ f c ≤ sSup (f '' Icc a b)

Proof state:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ f c ≤ sSup (f '' Icc a b)

Tactic:
exact this.2

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ f '' Icc a b
⊢ f c ≤ sSup (f '' Icc a b)

Tactic:
rw [h.image_Icc (hc.1.trans hc.2)] at this

Result:
α : Type u_2
β : Type u_3
inst✝⁶ : ConditionallyCompleteLinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : TopologicalSpace β
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ f c ≤ sSup (f '' Icc a b)