harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Range.lean
theorem ranges_length (l : List ℕ) :
    l.ranges.map length = l

Proof state:
case cons
a : ℕ
l : List ℕ
hl : map length l.ranges = l
⊢ map (length ∘ map fun x => a + x) l.ranges = map length l.ranges

Tactic:
apply map_congr_left

Result:
case cons.h
a : ℕ
l : List ℕ
hl : map length l.ranges = l
⊢ ∀ (a_1 : List ℕ), a_1 ∈ l.ranges → (length ∘ map fun x => a + x) a_1 = a_1.length

Proof state:
case cons
a : ℕ
l : List ℕ
hl : map length l.ranges = l
⊢ map (length ∘ map fun x => a + x) l.ranges = l

Tactic:
conv_rhs => rw [← hl]

Result:
case cons
a : ℕ
l : List ℕ
hl : map length l.ranges = l
⊢ map (length ∘ map fun x => a + x) l.ranges = map length l.ranges

Proof state:
case cons
a : ℕ
l : List ℕ
hl : map length l.ranges = l
⊢ map length (a :: l).ranges = a :: l

Tactic:
simp only [ranges, map_cons, length_range, map_map, cons.injEq, true_and]

Result:
case cons
a : ℕ
l : List ℕ
hl : map length l.ranges = l
⊢ map (length ∘ map fun x => a + x) l.ranges = l

Proof state:
l : List ℕ
⊢ map length l.ranges = l

Tactic:
induction l with
| nil => simp only [ranges, map_nil]
| cons a l hl => simp only [ranges, map_cons, length_range, map_map, cons.injEq, true_and]
  conv_rhs => rw [← hl]
  apply map_congr_left
  intro s _
  simp only [Function.comp_apply, length_map]

Result:
no goals

Proof state:
case cons.h
a : ℕ
l : List ℕ
hl : map length l.ranges = l
⊢ ∀ (a_1 : List ℕ), a_1 ∈ l.ranges → (length ∘ map fun x => a + x) a_1 = a_1.length

Tactic:
intro s _

Result:
case cons.h
a : ℕ
l : List ℕ
hl : map length l.ranges = l
s : List ℕ
a✝ : s ∈ l.ranges
⊢ (length ∘ map fun x => a + x) s = s.length

Proof state:
case cons.h
a : ℕ
l : List ℕ
hl : map length l.ranges = l
s : List ℕ
a✝ : s ∈ l.ranges
⊢ (length ∘ map fun x => a + x) s = s.length

Tactic:
simp only [Function.comp_apply, length_map]

Result:
no goals

Proof state:
case nil

⊢ map length [].ranges = []

Tactic:
simp only [ranges, map_nil]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
theorem homEquiv_naturality_left (f : X' ⟶ X) (g : F.obj X ⟶ Y) :
    (adj.homEquiv X' Y) (F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ (adj.homEquiv X' Y) (F.map f ≫ g) = f ≫ (adj.homEquiv X Y) g

Tactic:
rw [← Equiv.eq_symm_apply]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g = (adj.homEquiv X' Y).symm (f ≫ (adj.homEquiv X Y) g)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : CoreHomEquiv F G
X' X : C
Y : D
f : X' ⟶ X
g : F.obj X ⟶ Y
⊢ F.map f ≫ g = (adj.homEquiv X' Y).symm (f ≫ (adj.homEquiv X Y) g)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem AnalyticOnNhd.iterated_deriv [CompleteSpace F] (h : AnalyticOnNhd 𝕜 f s) (n : ℕ) :
    AnalyticOnNhd 𝕜 (deriv^[n] f) s

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
inst✝ : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
⊢ AnalyticOnNhd 𝕜 (deriv^[n] f) s

Tactic:
induction n with
| zero => exact h
| succ n IH => simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

Result:
no goals

Proof state:
case zero
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
inst✝ : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
⊢ AnalyticOnNhd 𝕜 (deriv^[0] f) s

Tactic:
exact h

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : 𝕜 → F
s : Set 𝕜
inst✝ : CompleteSpace F
h : AnalyticOnNhd 𝕜 f s
n : ℕ
IH : AnalyticOnNhd 𝕜 (deriv^[n] f) s
⊢ AnalyticOnNhd 𝕜 (deriv^[n + 1] f) s

Tactic:
simpa only [Function.iterate_succ', Function.comp_apply] using IH.deriv

Result:
no goals
-- Mathlib/RingTheory/ZMod.lean
theorem ZMod.ker_intCastRingHom (n : ℕ) :
    RingHom.ker (Int.castRingHom (ZMod n)) = Ideal.span ({(n : ℤ)} : Set ℤ)

Proof state:
n : ℕ
⊢ RingHom.ker (Int.castRingHom (ZMod n)) = Ideal.span {↑n}

Tactic:
ext

Result:
case h
n : ℕ
x✝ : ℤ
⊢ x✝ ∈ RingHom.ker (Int.castRingHom (ZMod n)) ↔ x✝ ∈ Ideal.span {↑n}

Proof state:
case h
n : ℕ
x✝ : ℤ
⊢ x✝ ∈ RingHom.ker (Int.castRingHom (ZMod n)) ↔ x✝ ∈ Ideal.span {↑n}

Tactic:
rw [Ideal.mem_span_singleton, RingHom.mem_ker, Int.coe_castRingHom,
  ZMod.intCast_zmod_eq_zero_iff_dvd]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/FixedPoint.lean
theorem iterate_le_nfp (f a n) : f^[n] a ≤ nfp f a

Proof state:
f : Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
n : ℕ
⊢ f^[n] a ≤ ⨆ n, f^[n] a

Tactic:
exact Ordinal.le_iSup (fun n ↦ f^[n] a) n

Result:
no goals

Proof state:
f : Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
n : ℕ
⊢ f^[n] a ≤ nfp f a

Tactic:
rw [← iSup_iterate_eq_nfp]

Result:
f : Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
n : ℕ
⊢ f^[n] a ≤ ⨆ n, f^[n] a
-- Mathlib/GroupTheory/Exponent.lean
theorem lcm_orderOf_dvd_exponent [Fintype G] :
    (Finset.univ : Finset G).lcm orderOf ∣ exponent G

Proof state:
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ Finset.univ.lcm orderOf ∣ exponent G

Tactic:
apply Finset.lcm_dvd

Result:
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ ∀ b ∈ Finset.univ, orderOf b ∣ exponent G

Proof state:
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
g : G
a✝ : g ∈ Finset.univ
⊢ orderOf g ∣ exponent G

Tactic:
exact order_dvd_exponent g

Result:
no goals

Proof state:
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ ∀ b ∈ Finset.univ, orderOf b ∣ exponent G

Tactic:
intro g _

Result:
case a
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
g : G
a✝ : g ∈ Finset.univ
⊢ orderOf g ∣ exponent G
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem areaForm_swap (x y : E) : ω x y = -ω y x

Proof state:
case h.e'_2.h.e'_6.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
i : Fin (Nat.succ 1)
⊢ ![x, y] i = (![y, x] ∘ ⇑(Equiv.swap 0 1)) i

Tactic:
fin_cases i <;> rfl

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.areaForm x) y = -(o.areaForm y) x

Tactic:
simp only [areaForm_to_volumeForm]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ o.volumeForm ![x, y] = -o.volumeForm ![y, x]

Proof state:
case h.e'_2.h.e'_6
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ![x, y] = ![y, x] ∘ ⇑(Equiv.swap 0 1)

Tactic:
ext i

Result:
case h.e'_2.h.e'_6.h
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
i : Fin (Nat.succ 1)
⊢ ![x, y] i = (![y, x] ∘ ⇑(Equiv.swap 0 1)) i

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ o.volumeForm ![x, y] = -o.volumeForm ![y, x]

Tactic:
convert o.volumeForm.map_swap ![y, x] (_ : (0 : Fin 2) ≠ 1)

Result:
case h.e'_2.h.e'_6
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ![x, y] = ![y, x] ∘ ⇑(Equiv.swap 0 1)

E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≠ 1

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ 0 ≠ 1

Tactic:
norm_num

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
/-- A constructor for `SMulPosMono` requiring you to prove `a₁ ≤ a₂ → a₁ • b ≤ a₂ • b` only when
`0 < b` -/
lemma SMulPosMono.of_pos (h₀ : ∀ b : β, 0 < b → ∀ a₁ a₂ : α, a₁ ≤ a₂ → a₁ • b ≤ a₂ • b) :
    SMulPosMono α β where
  elim b hb a₁ a₂ h

Proof state:
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
⊢ a₁ • b ≤ a₂ • b

Tactic:
obtain hb | hb := hb.eq_or_lt

Result:
case inl
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
hb : 0 = b
⊢ a₁ • b ≤ a₂ • b

case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
hb : 0 < b
⊢ a₁ • b ≤ a₂ • b

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
hb : 0 = b
⊢ a₁ • b ≤ a₂ • b

Tactic:
simp [← hb]

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Zero α
inst✝³ : Zero β
inst✝² : SMulWithZero α β
inst✝¹ : Preorder α
inst✝ : PartialOrder β
h₀ : ∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ ≤ a₂ → a₁ • b ≤ a₂ • b
b : β
hb✝ : 0 ≤ b
a₁ a₂ : α
h : a₁ ≤ a₂
hb : 0 < b
⊢ a₁ • b ≤ a₂ • b

Tactic:
exact h₀ _ hb _ _ h

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
lemma ext_of_mulVec_single [DecidableEq n] [Fintype n] {M N : Matrix m n α}
    (h : ∀ i, M *ᵥ Pi.single i 1 = N *ᵥ Pi.single i 1) :
    M = N

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M N : Matrix m n α
i : m
j : n
h : ∀ (i : n), Mᵀ i = Nᵀ i
⊢ M i j = N i j

Tactic:
exact congrFun (h j) i

Result:
no goals

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M N : Matrix m n α
h : ∀ (i : n), M *ᵥ Pi.single i 1 = N *ᵥ Pi.single i 1
i : m
j : n
⊢ M i j = N i j

Tactic:
simp_rw [mulVec_single_one] at h

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M N : Matrix m n α
i : m
j : n
h : ∀ (i : n), Mᵀ i = Nᵀ i
⊢ M i j = N i j

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M N : Matrix m n α
h : ∀ (i : n), M *ᵥ Pi.single i 1 = N *ᵥ Pi.single i 1
⊢ M = N

Tactic:
ext i j

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M N : Matrix m n α
h : ∀ (i : n), M *ᵥ Pi.single i 1 = N *ᵥ Pi.single i 1
i : m
j : n
⊢ M i j = N i j
-- Mathlib/ModelTheory/Types.lean
theorem setOf_subset_eq_univ_iff (S : L[[α]].Theory) :
    { p : T.CompleteType α | S ⊆ ↑p } = Set.univ ↔
      ∀ φ, φ ∈ S → (L.lhomWithConstants α).onTheory T ⊨ᵇ φ

Proof state:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
⊢ (∀ φ ∈ S, {p | φ ∈ p} = Set.univ) → ∀ s ∈ (fun φ => {p | φ ∈ p}) '' S, s = Set.univ

Tactic:
rintro h _ ⟨φ, h1, rfl⟩

Result:
case intro.intro
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h✝ : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
h : ∀ φ ∈ S, {p | φ ∈ p} = Set.univ
φ : L[[α]].Sentence
h1 : φ ∈ S
⊢ (fun φ => {p | φ ∈ p}) φ = Set.univ

Proof state:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
⊢ (∀ s ∈ (fun φ => {p | φ ∈ p}) '' S, s = Set.univ) ↔ ∀ φ ∈ S, {p | φ ∈ p} = Set.univ

Tactic:
refine ⟨fun h φ φS => h _ ⟨_, φS, rfl⟩, ?_⟩

Result:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
⊢ (∀ φ ∈ S, {p | φ ∈ p} = Set.univ) → ∀ s ∈ (fun φ => {p | φ ∈ p}) '' S, s = Set.univ

Proof state:
case h
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
x✝ : T.CompleteType α
⊢ x✝ ∈ {p | S ⊆ ↑p} ↔ x✝ ∈ ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)

Tactic:
simp [subset_def]

Result:
no goals

Proof state:
case intro.intro
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h✝ : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
h : ∀ φ ∈ S, {p | φ ∈ p} = Set.univ
φ : L[[α]].Sentence
h1 : φ ∈ S
⊢ (fun φ => {p | φ ∈ p}) φ = Set.univ

Tactic:
exact h _ h1

Result:
no goals

Proof state:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
⊢ {p | S ⊆ ↑p} = Set.univ ↔ ∀ φ ∈ S, (L.lhomWithConstants α).onTheory T ⊨ᵇ φ

Tactic:
simp_rw [h, sInter_eq_univ, ← setOf_mem_eq_univ_iff]

Result:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
⊢ (∀ s ∈ (fun φ => {p | φ ∈ p}) '' S, s = Set.univ) ↔ ∀ φ ∈ S, {p | φ ∈ p} = Set.univ

Proof state:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ {p | S ⊆ ↑p} = Set.univ ↔ ∀ φ ∈ S, (L.lhomWithConstants α).onTheory T ⊨ᵇ φ

Tactic:
have h : { p : T.CompleteType α | S ⊆ ↑p } = ⋂₀ ((fun φ => { p | φ ∈ p }) '' S) := by
  ext
  simp [subset_def]

Result:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
h : {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
⊢ {p | S ⊆ ↑p} = Set.univ ↔ ∀ φ ∈ S, (L.lhomWithConstants α).onTheory T ⊨ᵇ φ

Proof state:
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
⊢ {p | S ⊆ ↑p} = ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)

Tactic:
ext

Result:
case h
L : Language
T : L.Theory
α : Type w
S : L[[α]].Theory
x✝ : T.CompleteType α
⊢ x✝ ∈ {p | S ⊆ ↑p} ↔ x✝ ∈ ⋂₀ ((fun φ => {p | φ ∈ p}) '' S)
-- Mathlib/Data/Int/ModEq.lean
theorem add_modEq_left : n + a ≡ a [ZMOD n] := ModEq.symm <| modEq_iff_dvd.2 <| by simp

Proof state:
n a : ℤ
⊢ n ∣ n + a - a

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Interval.lean
theorem concat_right (hb : f ⊤ = g ⊥) {t : Icc a c} (ht : b ≤ t) :
    concat f g t = g ⟨t, ht, t.2.2⟩

Proof state:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
t : ↑(Icc a c)
ht : b ≤ ↑t
⊢ (f.concat g) t = g ⟨↑t, ⋯⟩

Tactic:
nth_rewrite 2 [← concat_comp_IccInclusionRight hb]

Result:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
t : ↑(Icc a c)
ht : b ≤ ↑t
⊢ (f.concat g) t = ((f.concat g).comp IccInclusionRight) ⟨↑t, ⋯⟩

Proof state:
α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
a b c : α
inst✝² : Fact (a ≤ b)
inst✝¹ : Fact (b ≤ c)
E : Type u_2
inst✝ : TopologicalSpace E
f : C(↑(Icc a b), E)
g : C(↑(Icc b c), E)
hb : f ⊤ = g ⊥
t : ↑(Icc a c)
ht : b ≤ ↑t
⊢ (f.concat g) t = ((f.concat g).comp IccInclusionRight) ⟨↑t, ⋯⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/ModelTheory/Definability.lean
theorem Definable.union {f g : Set (α → M)} (hf : A.Definable L f) (hg : A.Definable L g) :
    A.Definable L (f ∪ g)

Proof state:
case intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
hg : A.Definable L g
φ : L[[↑A]].Formula α
hφ : f = setOf φ.Realize
⊢ A.Definable L (f ∪ g)

Tactic:
rcases hg with ⟨θ, hθ⟩

Result:
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
φ : L[[↑A]].Formula α
hφ : f = setOf φ.Realize
θ : L[[↑A]].Formula α
hθ : g = setOf θ.Realize
⊢ A.Definable L (f ∪ g)

Proof state:
case intro.intro.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
φ : L[[↑A]].Formula α
hφ : f = setOf φ.Realize
θ : L[[↑A]].Formula α
hθ : g = setOf θ.Realize
x✝ : α → M
⊢ x✝ ∈ f ∪ g ↔ x✝ ∈ setOf (φ ⊔ θ).Realize

Tactic:
rw [hφ, hθ, mem_setOf_eq, Formula.realize_sup, mem_union, mem_setOf_eq, mem_setOf_eq]

Result:
no goals

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
hf : A.Definable L f
hg : A.Definable L g
⊢ A.Definable L (f ∪ g)

Tactic:
rcases hf with ⟨φ, hφ⟩

Result:
case intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
hg : A.Definable L g
φ : L[[↑A]].Formula α
hφ : f = setOf φ.Realize
⊢ A.Definable L (f ∪ g)

Proof state:
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
φ : L[[↑A]].Formula α
hφ : f = setOf φ.Realize
θ : L[[↑A]].Formula α
hθ : g = setOf θ.Realize
⊢ A.Definable L (f ∪ g)

Tactic:
refine ⟨φ ⊔ θ, ?_⟩

Result:
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
φ : L[[↑A]].Formula α
hφ : f = setOf φ.Realize
θ : L[[↑A]].Formula α
hθ : g = setOf θ.Realize
⊢ f ∪ g = setOf (φ ⊔ θ).Realize

Proof state:
case intro.intro
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
φ : L[[↑A]].Formula α
hφ : f = setOf φ.Realize
θ : L[[↑A]].Formula α
hθ : g = setOf θ.Realize
⊢ f ∪ g = setOf (φ ⊔ θ).Realize

Tactic:
ext

Result:
case intro.intro.h
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
f g : Set (α → M)
φ : L[[↑A]].Formula α
hφ : f = setOf φ.Realize
θ : L[[↑A]].Formula α
hθ : g = setOf θ.Realize
x✝ : α → M
⊢ x✝ ∈ f ∪ g ↔ x✝ ∈ setOf (φ ⊔ θ).Realize
-- Mathlib/FieldTheory/Galois/Basic.lean
theorem mem_fixedField_iff (x) :
    x ∈ fixedField H ↔ ∀ f ∈ H, f x = x

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
x : E
⊢ x ∈ fixedField H ↔ ∀ f ∈ H, f x = x

Tactic:
show x ∈ MulAction.fixedPoints H E ↔ _

Result:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
x : E
⊢ x ∈ MulAction.fixedPoints (↥H) E ↔ ∀ f ∈ H, f x = x

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
H : Subgroup (E ≃ₐ[F] E)
x : E
⊢ x ∈ MulAction.fixedPoints (↥H) E ↔ ∀ f ∈ H, f x = x

Tactic:
simp only [MulAction.mem_fixedPoints, Subtype.forall, Subgroup.mk_smul, AlgEquiv.smul_def]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem j_of_isShortNF : W.j = 6912 * W.a₄ ^ 3 / (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

Proof state:
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsShortNF
h : ↑W.Δ' ≠ 0
⊢ W.j = 6912 * W.a₄ ^ 3 / (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

Tactic:
rw [coe_Δ', Δ_of_isShortNF] at h

Result:
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsShortNF
h : -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) ≠ 0
⊢ W.j = 6912 * W.a₄ ^ 3 / (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

Proof state:
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsShortNF
h : -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) ≠ 0
⊢ (-48 * W.a₄) ^ 3 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) = 6912 * W.a₄ ^ 3 * (-16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2))

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsShortNF
h : -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) ≠ 0
⊢ W.j = 6912 * W.a₄ ^ 3 / (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

Tactic:
rw [j, Units.val_inv_eq_inv_val, ← div_eq_inv_mul, coe_Δ',
  c₄_of_isShortNF, Δ_of_isShortNF, div_eq_div_iff h (right_ne_zero_of_mul h)]

Result:
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsShortNF
h : -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) ≠ 0
⊢ (-48 * W.a₄) ^ 3 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) = 6912 * W.a₄ ^ 3 * (-16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2))

Proof state:
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsShortNF
⊢ W.j = 6912 * W.a₄ ^ 3 / (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

Tactic:
have h := W.Δ'.ne_zero

Result:
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsShortNF
h : ↑W.Δ' ≠ 0
⊢ W.j = 6912 * W.a₄ ^ 3 / (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)
-- Mathlib/Data/Int/CardIntervalMod.lean
lemma Ico_filter_modEq_eq (v : ℤ) :
    {x ∈ Ico a b | x ≡ v [ZMOD r]} =
    {x ∈ Ico (a - v) (b - v) | r ∣ x}.map ⟨(· + v), add_left_injective v⟩

Proof state:
a b r v : ℤ
⊢ filter (fun x => x ≡ v [ZMOD r]) (Ico a b) =
    map { toFun := fun x => x + v, inj' := ⋯ } (filter (fun x => r ∣ x) (Ico (a - v) (b - v)))

Tactic:
ext x

Result:
case h
a b r v x : ℤ
⊢ x ∈ filter (fun x => x ≡ v [ZMOD r]) (Ico a b) ↔
    x ∈ map { toFun := fun x => x + v, inj' := ⋯ } (filter (fun x => r ∣ x) (Ico (a - v) (b - v)))

Proof state:
case h
a b r v x : ℤ
⊢ x ∈ filter (fun x => x ≡ v [ZMOD r]) (Ico a b) ↔
    x ∈ map { toFun := fun x => x + v, inj' := ⋯ } (filter (fun x => r ∣ x) (Ico (a - v) (b - v)))

Tactic:
simp_rw [mem_map, mem_filter, mem_Ico, Function.Embedding.coeFn_mk, ← eq_sub_iff_add_eq,
  exists_eq_right, modEq_comm, modEq_iff_dvd, sub_lt_sub_iff_right, sub_le_sub_iff_right]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem EuclideanSpace.inner_single_right (i : ι) (a : 𝕜) (v : EuclideanSpace 𝕜 ι) :
    ⟪v, EuclideanSpace.single i (a : 𝕜)⟫ = a * conj (v i)

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
a : 𝕜
v : EuclideanSpace 𝕜 ι
⊢ inner v (single i a) = a * (starRingEnd ((fun x => 𝕜) i)) (v i)

Tactic:
simp [apply_ite conj, mul_comm]

Result:
no goals
-- Mathlib/Order/RelSeries.lean
lemma nonempty_of_finiteDimensionalOrder [FiniteDimensionalOrder α] : Nonempty α

Proof state:
case intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
p : RelSeries fun x1 x2 => x1 < x2
h✝ : ∀ (y : RelSeries fun x1 x2 => x1 < x2), y.length ≤ p.length
⊢ Nonempty α

Tactic:
exact ⟨p 0⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
⊢ Nonempty α

Tactic:
obtain ⟨p, _⟩ := (Rel.finiteDimensional_iff _).mp ‹_›

Result:
case intro
α : Type u_1
inst✝¹ : Preorder α
inst✝ : FiniteDimensionalOrder α
p : RelSeries fun x1 x2 => x1 < x2
h✝ : ∀ (y : RelSeries fun x1 x2 => x1 < x2), y.length ≤ p.length
⊢ Nonempty α
-- Mathlib/Analysis/Convex/Basic.lean
theorem convex_iff_ordConnected [LinearOrderedField 𝕜] {s : Set 𝕜} :
    Convex 𝕜 s ↔ s.OrdConnected

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
⊢ Convex 𝕜 s ↔ s.OrdConnected

Tactic:
simp_rw [convex_iff_segment_subset, segment_eq_uIcc, ordConnected_iff_uIcc_subset]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Map.lean
theorem comap_id (K : Subgroup N) : K.comap (MonoidHom.id _) = K

Proof state:
case h
N : Type u_5
inst✝ : Group N
K : Subgroup N
x✝ : N
⊢ x✝ ∈ comap (MonoidHom.id N) K ↔ x✝ ∈ K

Tactic:
rfl

Result:
no goals

Proof state:
N : Type u_5
inst✝ : Group N
K : Subgroup N
⊢ comap (MonoidHom.id N) K = K

Tactic:
ext

Result:
case h
N : Type u_5
inst✝ : Group N
K : Subgroup N
x✝ : N
⊢ x✝ ∈ comap (MonoidHom.id N) K ↔ x✝ ∈ K